12 A :: i => i => i |
12 A :: i => i => i |
13 B :: i => i => i |
13 B :: i => i => i |
14 C :: i => i |
14 C :: i => i |
15 Gamma :: [i,i,i] => i |
15 Gamma :: [i,i,i] => i |
16 |
16 |
17 rules (*NOT definitional*) |
17 rules (*NOT definitional*) |
18 A_nat_def "A(N(n)) == (%sigma. n)" |
18 A_nat_def "A(N(n)) == (%sigma. n)" |
19 A_loc_def "A(X(x)) == (%sigma. sigma`x)" |
19 A_loc_def "A(X(x)) == (%sigma. sigma`x)" |
20 A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))" |
20 A_op1_def "A(Op1(f,a)) == (%sigma. f`A(a,sigma))" |
21 A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" |
21 A_op2_def "A(Op2(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" |
22 |
22 |
23 |
23 |
24 B_true_def "B(true) == (%sigma. 1)" |
24 B_true_def "B(true) == (%sigma. 1)" |
25 B_false_def "B(false) == (%sigma. 0)" |
25 B_false_def "B(false) == (%sigma. 0)" |
26 B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" |
26 B_op_def "B(ROp(f,a0,a1)) == (%sigma. f`<A(a0,sigma),A(a1,sigma)>)" |
27 |
27 |
28 |
28 |
29 B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))" |
29 B_not_def "B(noti(b)) == (%sigma. not(B(b,sigma)))" |
30 B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))" |
30 B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) and B(b1,sigma))" |
31 B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))" |
31 B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))" |
32 |
32 |
33 C_skip_def "C(skip) == id(loc->nat)" |
33 C_skip_def "C(skip) == id(loc->nat)" |
34 C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat). |
34 C_assign_def "C(x := a) == {io:(loc->nat)*(loc->nat). |
35 snd(io) = fst(io)[A(a,fst(io))/x]}" |
35 snd(io) = fst(io)[A(a,fst(io))/x]}" |
36 |
36 |
37 C_comp_def "C(c0 ; c1) == C(c1) O C(c0)" |
37 C_comp_def "C(c0 ; c1) == C(c1) O C(c0)" |
38 C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un |
38 C_if_def "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un |
39 {io:C(c1). B(b,fst(io))=0}" |
39 {io:C(c1). B(b,fst(io))=0}" |
40 |
40 |
41 Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un |
41 Gamma_def "Gamma(b,c) == (%phi.{io : (phi O C(c)). B(b,fst(io))=1} Un |
42 {io : id(loc->nat). B(b,fst(io))=0})" |
42 {io : id(loc->nat). B(b,fst(io))=0})" |
43 |
43 |
44 C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))" |
44 C_while_def "C(while b do c) == lfp((loc->nat)*(loc->nat), Gamma(b,c))" |
45 |
45 |
46 end |
46 end |