forked from runtimeverification/zero-to-k-tutorial
-
Notifications
You must be signed in to change notification settings - Fork 0
/
06_procedures.k.sol
129 lines (102 loc) · 4.07 KB
/
06_procedures.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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
module PROCEDURES-SYNTAX
imports INT-SYNTAX
imports BOOL-SYNTAX
imports ID
syntax Exp ::= IExp | BExp
syntax IExp ::= Id | Int
syntax KResult ::= Int | Bool | Ints
// Take this sort structure:
//
// IExp
// / \
// Int Id
//
// Through the List{_, ","} functor.
// Must add a `Bot`, for a common subsort for the empty list.
syntax Bot
syntax Bots ::= List{Bot, ","} [klabel(exps)]
syntax Ints ::= List{Int, ","} [klabel(exps)]
| Bots
syntax Ids ::= List{Id, ","} [klabel(exps)]
| Bots
syntax Exps ::= List{Exp, ","} [klabel(exps), seqstrict]
| Ids | Ints
syntax IExp ::= "(" IExp ")" [bracket]
| IExp "+" IExp [strict]
| IExp "-" IExp [strict]
> IExp "*" IExp [strict]
| IExp "/" IExp [strict]
> IExp "^" IExp [strict]
| Id "(" Exps ")" [strict(2)]
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
| BExp "||" BExp
syntax Stmt ::= Id "=" IExp ";" [strict(2)]
| Stmt Stmt [left]
| Block
| "if" "(" BExp ")" Block "else" Block [strict(1)]
| "while" "(" BExp ")" Block
| "return" IExp ";" [strict]
| "def" Id "(" Ids ")" Block
syntax Block ::= "{" Stmt "}" | "{" "}"
endmodule
module PROCEDURES
imports INT
imports BOOL
imports MAP
imports PROCEDURES-SYNTAX
configuration
<k> $PGM:Stmt </k>
<mem> .Map </mem>
<funcs> .Map </funcs>
<stack> .List </stack>
// -----------------------------------------------
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>
rule <k> def FNAME ( ARGS ) BODY => . ... </k>
<funcs> FS => FS [ FNAME <- def FNAME ( ARGS ) BODY ] </funcs>
rule <k> FNAME ( IS:Ints ) ~> CONT => #makeBindings(ARGS, IS) ~> BODY </k>
<funcs> ... FNAME |-> def FNAME ( ARGS ) BODY ... </funcs>
<mem> MEM => .Map </mem>
<stack> .List => ListItem(state(CONT, MEM)) ... </stack>
rule <k> return I:Int ; ~> _ => I ~> CONT </k>
<stack> ListItem(state(CONT, MEM)) => .List ... </stack>
<mem> _ => MEM </mem>
rule <k> return I:Int ; ~> . => I </k>
<stack> .List </stack>
syntax KItem ::= #makeBindings(Ids, Ints)
| state(continuation: K, memory: Map)
// ----------------------------------------------------
rule <k> #makeBindings(.Ids, .Ints) => . ... </k>
rule <k> #makeBindings((I:Id, IDS => IDS), (IN:Int, INTS => INTS)) ... </k>
<mem> MEM => MEM [ I <- IN ] </mem>
endmodule