6 <e,o> |> v means that e evaluates to v in the state o.
11 basic arithmetic operations.
14 <e1 + e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is the sum of v1 and v2
18 <e1 - e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is v1 subtracted from v2
22 <e1 * e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is the product of v1 and v2
26 <e1 / e2, o> |> v <= <e1,o> |> v1 & <e2,o> |> v2 & v is v1 divided by v2
30 basic comparative operations.
35 <e1 < e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is smaller than v2
36 <e1 < e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is larger than or as large as v2
38 <e1 <= e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is smaller than or as small as v2
39 <e1 <= e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is larger than v2
41 +similar rules apply for greater than+
46 <e1 == e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is equal to v2
47 <e1 == e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is not equal to v2
49 <e1 != e2, o> |> true <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is not equal to to v2
50 <e1 != e2, o> |> false <= <e1,o> |> v1 & <e2,o> |> v2 & v1 is equal to v2
56 <!e, o> |> false <= <e,o> |> true
57 <!e, o> |> true <= <e,o> |> false
59 <-e, o> |> v2 <= <e,o> |> v1 & v2 is the negative value of v1
75 <if e s1 else s2, o> |> o' <= <e,o> |> true & <s1, o> |> o'
76 <if e s1 else s2, o> |> o' <= <e,o> |> false & <s2, o> |> o'
79 <while e s, o> |> o'' <= <e,o> |> true & <s,o> |> o' & <while e s, o'> |> o''
80 <while e s, o> |> o <= <e,o> |> false
83 <x = e, o> |> o[x->v] <= <e,o> |> v
86 <s1; s2, o> |> o'' <= <s1,o> |> o' & <s2, o'> |> o''