equal
deleted
inserted
replaced
8 |
8 |
9 Denotation = Com + |
9 Denotation = Com + |
10 |
10 |
11 types com_den = "(state*state)set" |
11 types com_den = "(state*state)set" |
12 consts |
12 consts |
13 A :: "aexp => state => nat" |
13 A :: aexp => state => nat |
14 B :: "bexp => state => bool" |
14 B :: bexp => state => bool |
15 C :: "com => com_den" |
15 C :: com => com_den |
16 Gamma :: "[bexp,com_den] => (com_den => com_den)" |
16 Gamma :: [bexp,com_den] => (com_den => com_den) |
17 |
17 |
18 primrec A aexp |
18 primrec A aexp |
19 A_nat "A(N(n)) = (%s. n)" |
19 A_nat "A(N(n)) = (%s. n)" |
20 A_loc "A(X(x)) = (%s. s(x))" |
20 A_loc "A(X(x)) = (%s. s(x))" |
21 A_op1 "A(Op1 f a) = (%s. f(A a s))" |
21 A_op1 "A(Op1 f a) = (%s. f(A a s))" |