Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
75 lines (68 sloc) 2.28 KB
// Adapted from the K tutorial examples at
// https://github.com/kframework/k/tree/master/k-distribution/tutorial
module IMP-SYNTAX
imports DOMAINS-SYNTAX
imports INT-SYNTAX
syntax AExp ::= Int | Id
| AExp "/" AExp [left, strict]
> AExp "+" AExp [left, strict]
| "(" AExp ")" [bracket]
syntax BExp ::= Bool
| AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})]
| "!" BExp [strict]
> BExp "&&" BExp [left, strict(1)]
| "(" BExp ")" [bracket]
syntax Block ::= "{" "}"
| "{" Stmt "}"
syntax Stmt ::= Block
| Id "=" AExp ";" [strict(2)]
| "if" "(" BExp ")"
Block "else" Block [strict(1)]
| "while" "(" BExp ")" Block
> Stmt Stmt [left]
syntax Pgm ::= "int" Ids ";" Stmt
syntax Ids ::= List{Id,","}
endmodule
module IMP
imports IMP-SYNTAX
imports DOMAINS
syntax KResult ::= Int | Bool
configuration <T color="yellow">
<k color="green"> $PGM:Pgm </k>
<state color="red"> .Map </state>
</T>
// AExp
rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
rule I1 / I2 => I1 /Int I2 requires I2 =/=Int 0
rule I1 + I2 => I1 +Int I2
// BExp
rule I1 <= I2 => I1 <=Int I2
rule ! T => notBool T
rule true && B => B
rule false && _ => false
// Block
rule {} => . [structural]
rule {S} => S [structural]
// Stmt
rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
rule S1:Stmt S2:Stmt => S1 ~> S2 [structural]
rule if (true) S else _ => S
rule if (false) _ else S => S
rule while (B) S => if (B) {S while (B) S} else {} [structural]
// Pgm
rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
requires notBool (X in keys(Rho))
rule int .Ids; S => S [structural]
// verification example
syntax Id ::= "n" [token]
| "sum" [token]
syntax Pgm ::= "sum_pgm" Int [macro]
rule sum_pgm N =>
int n, sum;
n = N;
sum = 0;
while (!(n <= 0)) {
sum = sum + n;
n = n + (-1);
}
endmodule
You can’t perform that action at this time.