|
1 (* Title: ZF/IMP/Denotation.thy |
|
2 ID: $Id$ |
|
3 Author: Heiko Loetzbeyer & Robert Sandner, TUM |
|
4 Copyright 1994 TUM |
|
5 |
|
6 Denotational semantics of expressions & commands |
|
7 *) |
|
8 |
|
9 Denotation = Com + |
|
10 |
|
11 consts |
|
12 A :: "aexp => env => nat" |
|
13 B :: "bexp => env => bool" |
|
14 C :: "com => (env*env)set" |
|
15 Gamma :: "[bexp,com,(env*env)set] => (env*env)set" |
|
16 |
|
17 rules |
|
18 A_nat_def "A(N(n)) == (%sigma. n)" |
|
19 A_loc_def "A(X(x)) == (%sigma. sigma(x))" |
|
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)))" |
|
22 |
|
23 |
|
24 B_true_def "B(true) == (%sigma. True)" |
|
25 B_false_def "B(false) == (%sigma. False)" |
|
26 B_op_def "B(ROp(f,a0,a1)) == (%sigma. f(A(a0,sigma),A(a1,sigma)))" |
|
27 |
|
28 |
|
29 B_not_def "B(noti(b)) == (%sigma. ~B(b,sigma))" |
|
30 B_and_def "B(b0 andi b1) == (%sigma. B(b0,sigma) & B(b1,sigma))" |
|
31 B_or_def "B(b0 ori b1) == (%sigma. B(b0,sigma) | B(b1,sigma))" |
|
32 |
|
33 C_skip_def "C(skip) == id" |
|
34 C_assign_def "C(x := a) == {io . snd(io) = fst(io)[A(a,fst(io))/x]}" |
|
35 |
|
36 C_comp_def "C(c0 ; c1) == C(c1) O C(c0)" |
|
37 C_if_def "C(ifc b then c0 else c1) == \ |
|
38 \ {io. io:C(c0) & B(b,fst(io))} Un \ |
|
39 \ {io. io:C(c1) & ~B(b,fst(io))}" |
|
40 |
|
41 Gamma_def "Gamma(b,c) == \ |
|
42 \ (%phi.{io. io : (phi O C(c)) & B(b,fst(io))} Un \ |
|
43 \ {io. io : id & ~B(b,fst(io))})" |
|
44 |
|
45 C_while_def "C(while b do c) == lfp(Gamma(b,c))" |
|
46 |
|
47 end |