forked from runtimeverification/zero-to-k-tutorial
-
Notifications
You must be signed in to change notification settings - Fork 0
/
02_calc-bool.k.sol
46 lines (38 loc) · 1.26 KB
/
02_calc-bool.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
module CALC-BOOL-SYNTAX
imports INT-SYNTAX
imports BOOL-SYNTAX
syntax Exp ::= Int | Bool
syntax Int ::= "(" Int ")" [bracket]
| Int "+" Int [function]
| Int "-" Int [function]
> Int "*" Int [function]
| Int "/" Int [function]
> Int "^" Int [function]
syntax Bool ::= "(" Bool ")" [bracket]
| Int "<=" Int [function]
| Int "<" Int [function]
| Int ">=" Int [function]
| Int ">" Int [function]
| Int "==" Int [function]
| Int "!=" Int [function]
syntax Bool ::= Bool "&&" Bool [function]
| Bool "||" Bool [function]
endmodule
module CALC-BOOL
imports INT
imports BOOL
imports CALC-BOOL-SYNTAX
rule I1 + I2 => I1 +Int I2
rule I1 - I2 => I1 -Int I2
rule I1 * I2 => I1 *Int I2
rule I1 / I2 => I1 /Int I2
rule I1 ^ I2 => I1 ^Int I2
rule I1 <= I2 => I1 <=Int I2
rule I1 < I2 => I1 <Int I2
rule I1 >= I2 => I1 >=Int I2
rule I1 > I2 => I1 >Int I2
rule I1 == I2 => I1 ==Int I2
rule I1 != I2 => I1 =/=Int I2
rule B1 && B2 => B1 andBool B2
rule B1 || B2 => B1 orBool B2
endmodule