20 vc,wp :: acom => assn => assn |
20 vc,wp :: acom => assn => assn |
21 vcwp :: "acom => assn => assn * assn" |
21 vcwp :: "acom => assn => assn * assn" |
22 astrip :: acom => com |
22 astrip :: acom => com |
23 |
23 |
24 primrec wp acom |
24 primrec wp acom |
25 wp_Askip "wp Askip Q = Q" |
25 "wp Askip Q = Q" |
26 wp_Aass "wp (Aass x a) Q = (%s.Q(s[a s/x]))" |
26 "wp (Aass x a) Q = (%s.Q(s[a s/x]))" |
27 wp_Asemi "wp (Asemi c d) Q = wp c (wp d Q)" |
27 "wp (Asemi c d) Q = wp c (wp d Q)" |
28 wp_Aif "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" |
28 "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" |
29 wp_Awhile "wp (Awhile b I c) Q = I" |
29 "wp (Awhile b I c) Q = I" |
30 |
30 |
31 primrec vc acom |
31 primrec vc acom |
32 vc_Askip "vc Askip Q = (%s.True)" |
32 "vc Askip Q = (%s.True)" |
33 vc_Aass "vc (Aass x a) Q = (%s.True)" |
33 "vc (Aass x a) Q = (%s.True)" |
34 vc_Asemi "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)" |
34 "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)" |
35 vc_Aif "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" |
35 "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" |
36 vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) & |
36 "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) & |
37 (I s & b s --> wp c I s) & vc c I s)" |
37 (I s & b s --> wp c I s) & vc c I s)" |
38 |
38 |
39 primrec astrip acom |
39 primrec astrip acom |
40 astrip_Askip "astrip Askip = SKIP" |
40 "astrip Askip = SKIP" |
41 astrip_Aass "astrip (Aass x a) = (x:=a)" |
41 "astrip (Aass x a) = (x:=a)" |
42 astrip_Asemi "astrip (Asemi c d) = (astrip c;astrip d)" |
42 "astrip (Asemi c d) = (astrip c;astrip d)" |
43 astrip_Aif "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)" |
43 "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)" |
44 astrip_Awhile "astrip (Awhile b I c) = (WHILE b DO astrip c)" |
44 "astrip (Awhile b I c) = (WHILE b DO astrip c)" |
45 |
45 |
46 (* simultaneous computation of vc and wp: *) |
46 (* simultaneous computation of vc and wp: *) |
47 primrec vcwp acom |
47 primrec vcwp acom |
48 vcwp_Askip |
|
49 "vcwp Askip Q = (%s.True, Q)" |
48 "vcwp Askip Q = (%s.True, Q)" |
50 vcwp_Aass |
|
51 "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))" |
49 "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))" |
52 vcwp_Asemi |
|
53 "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q; |
50 "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q; |
54 (vcc,wpc) = vcwp c wpd |
51 (vcc,wpc) = vcwp c wpd |
55 in (%s. vcc s & vcd s, wpc))" |
52 in (%s. vcc s & vcd s, wpc))" |
56 vcwp_Aif |
|
57 "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q; |
53 "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q; |
58 (vcc,wpc) = vcwp c Q |
54 (vcc,wpc) = vcwp c Q |
59 in (%s. vcc s & vcd s, |
55 in (%s. vcc s & vcd s, |
60 %s.(b s-->wpc s) & (~b s-->wpd s)))" |
56 %s.(b s-->wpc s) & (~b s-->wpd s)))" |
61 vcwp_Awhile |
|
62 "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I |
57 "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I |
63 in (%s. (I s & ~b s --> Q s) & |
58 in (%s. (I s & ~b s --> Q s) & |
64 (I s & b s --> wpc s) & vcc s, I))" |
59 (I s & b s --> wpc s) & vcc s, I))" |
65 |
60 |
66 end |
61 end |