equal
deleted
inserted
replaced
16 | Aif bexp acom acom |
16 | Aif bexp acom acom |
17 | Awhile bexp assn acom |
17 | Awhile bexp assn acom |
18 |
18 |
19 consts |
19 consts |
20 vc,wp :: acom => assn => assn |
20 vc,wp :: acom => assn => assn |
|
21 vcwp :: "acom => assn => assn * assn" |
21 astrip :: acom => com |
22 astrip :: acom => com |
22 |
23 |
23 primrec wp acom |
24 primrec wp acom |
24 wp_Askip "wp Askip Q = Q" |
25 wp_Askip "wp Askip Q = Q" |
25 wp_Aass "wp (Aass x a) Q = (%s.Q(s[A a s/x]))" |
26 wp_Aass "wp (Aass x a) Q = (%s.Q(s[A a s/x]))" |
39 astrip_Askip "astrip Askip = skip" |
40 astrip_Askip "astrip Askip = skip" |
40 astrip_Aass "astrip (Aass x a) = (x:=a)" |
41 astrip_Aass "astrip (Aass x a) = (x:=a)" |
41 astrip_Asemi "astrip (Asemi c d) = (astrip c;astrip d)" |
42 astrip_Asemi "astrip (Asemi c d) = (astrip c;astrip d)" |
42 astrip_Aif "astrip (Aif b c d) = ifC b (astrip c) (astrip d)" |
43 astrip_Aif "astrip (Aif b c d) = ifC b (astrip c) (astrip d)" |
43 astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)" |
44 astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)" |
44 |
45 |
|
46 (* simultaneous computation of vc and wp: *) |
|
47 primrec vcwp acom |
|
48 vcwp_Askip |
|
49 "vcwp Askip Q = (%s.True, Q)" |
|
50 vcwp_Aass |
|
51 "vcwp (Aass x a) Q = (%s.True, %s.Q(s[A a s/x]))" |
|
52 vcwp_Asemi |
|
53 "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q; |
|
54 (vcc,wpc) = vcwp c wpd |
|
55 in (%s. vcc s & vcd s, wpc))" |
|
56 vcwp_Aif |
|
57 "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q; |
|
58 (vcc,wpc) = vcwp c Q |
|
59 in (%s. vcc s & vcd s, |
|
60 %s.(B b s-->wpc s) & (~B b s-->wpd s)))" |
|
61 vcwp_Awhile |
|
62 "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I |
|
63 in (%s. (I s & ~B b s --> Q s) & |
|
64 (I s & B b s --> wpc s) & vcc s, I))" |
|
65 |
45 end |
66 end |