forked from runtimeverification/zero-to-k-tutorial
-
Notifications
You must be signed in to change notification settings - Fork 0
/
05_control-flow.k.sol
83 lines (64 loc) · 2.45 KB
/
05_control-flow.k.sol
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
module CONTROL-FLOW-SYNTAX
imports INT-SYNTAX
imports BOOL-SYNTAX
imports ID
syntax Exp ::= IExp | BExp
syntax IExp ::= Id | Int
syntax KResult ::= Int | Bool
syntax IExp ::= "(" IExp ")" [bracket]
| IExp "+" IExp [strict]
| IExp "-" IExp [strict]
> IExp "*" IExp [strict]
| IExp "/" IExp [strict]
> IExp "^" IExp [strict]
syntax BExp ::= Bool
syntax BExp ::= "(" BExp ")" [bracket]
| IExp "<=" IExp [strict]
| IExp "<" IExp [strict]
| IExp ">=" IExp [strict]
| IExp ">" IExp [strict]
| IExp "==" IExp [strict]
| IExp "!=" IExp [strict]
syntax BExp ::= BExp "&&" BExp [strict]
| BExp "||" BExp [strict]
syntax Stmt ::= Id "=" IExp ";" [strict(2)]
| Stmt Stmt [left]
| "{" Stmt "}"
| "{" "}"
| "if" "(" BExp ")" Stmt "else" Stmt [strict(1)]
| "while" "(" BExp ")" Stmt
endmodule
module CONTROL-FLOW
imports INT
imports BOOL
imports MAP
imports CONTROL-FLOW-SYNTAX
configuration
<k> $PGM:Stmt </k>
<mem> .Map </mem>
// -----------------------------------------------
rule <k> I1 + I2 => I1 +Int I2 ... </k>
rule <k> I1 - I2 => I1 -Int I2 ... </k>
rule <k> I1 * I2 => I1 *Int I2 ... </k>
rule <k> I1 / I2 => I1 /Int I2 ... </k>
rule <k> I1 ^ I2 => I1 ^Int I2 ... </k>
rule <k> I:Id => MEM[I] ... </k>
<mem> MEM </mem>
// ------------------------------------------------
rule <k> I1 <= I2 => I1 <=Int I2 ... </k>
rule <k> I1 < I2 => I1 <Int I2 ... </k>
rule <k> I1 >= I2 => I1 >=Int I2 ... </k>
rule <k> I1 > I2 => I1 >Int I2 ... </k>
rule <k> I1 == I2 => I1 ==Int I2 ... </k>
rule <k> I1 != I2 => I1 =/=Int I2 ... </k>
rule <k> B1 && B2 => B1 andBool B2 ... </k>
rule <k> B1 || B2 => B1 orBool B2 ... </k>
rule <k> S1:Stmt S2:Stmt => S1 ~> S2 ... </k>
rule <k> ID = I:Int ; => . ... </k>
<mem> MEM => MEM [ ID <- I ] </mem>
rule <k> { S } => S ... </k>
rule <k> { } => . ... </k>
rule <k> if (true) THEN else _ELSE => THEN ... </k>
rule <k> if (false) _THEN else ELSE => ELSE ... </k>
rule <k> while ( BE ) BODY => if ( BE ) { BODY while ( BE ) BODY } else { } ... </k>
endmodule