Skip to content

Latest commit

 

History

History
84 lines (62 loc) · 1.96 KB

kat-fun.md

File metadata and controls

84 lines (62 loc) · 1.96 KB

Instantiation of KAT

The KAT requires some programming-language specific information to work. Instantiation of the progamming language to KAT should happen with the language semantics on an as-needed basis.

The module FUN-KAT includes all the supported analysis for the FUN language.

requires "fun.k"
requires "kat.k"

module FUN-ANALYSIS
    imports STRATEGY
    imports FUN-SBC
endmodule

module FUN-KAT
    imports FUN-UNTYPED
    imports KAT

    configuration <kat-FUN> initSCell(Init) initKatCell <harness> initFUNCell(Init) </harness> </kat-FUN>

Define push and pop

Here the definition of a State for FUN is given, as well as the definitions of how to push and pop states.

    syntax PreState ::= FUNCell
 // ---------------------------
    rule <s> push         => push FUNCELL ... </s> <harness> FUNCELL </harness>
    rule <s> pop  FUNCELL => .            ... </s> <harness> _ => FUNCELL </harness>

Define #branch and #normal

    rule #normal => ^ lookup | ^ assignment
    rule #branch => ^ iftrue | ^ iffalse
    rule #loop   => ^ letRecursive

Define bool?

    rule <s> bool? [ <FUN> <k> true  ... </k> ... </FUN> ] => #true  ... </s>
    rule <s> bool? [ <FUN> <k> false ... </k> ... </FUN> ] => #false ... </s>
endmodule

SBC

module FUN-SBC
    imports FUN-KAT
    imports KAT-SBC
    imports MATCHING

Define abstract

    rule <s> abstract [ STATE ] => pop STATE ... </s>

Define _subsumes?_

Subsumption will be based on matching one <k> cell with the other. This is correct because the memory is fully abstracted at the beginning of each rule.

TODO: We should be able to match on the entire configuration, not just the <k> cell.

    rule <s> <FUN> <k> KCELL </k> ... </FUN> subsumes? <FUN> <k> KCELL' </k> ... </FUN>
          => #if #matches(KCELL', KCELL) #then #true #else #false #fi
         ...
         </s>

endmodule