equal
deleted
inserted
replaced
35 vc_Aif "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" |
35 vc_Aif "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 b s --> Q s) & |
36 vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) & |
37 (I s & B b s --> wp c I s) & vc c I s)" |
37 (I s & B 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 "astrip Askip = Skip" |
41 astrip_Aass "astrip (Aass x a) = (x:=a)" |
41 astrip_Aass "astrip (Aass x a) = (x:=a)" |
42 astrip_Asemi "astrip (Asemi c d) = (astrip c;astrip d)" |
42 astrip_Asemi "astrip (Asemi c d) = (astrip c;astrip d)" |
43 astrip_Aif "astrip (Aif b c d) = ifC b (astrip c) (astrip d)" |
43 astrip_Aif "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)" |
44 astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)" |
44 astrip_Awhile "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 |
48 vcwp_Askip |
49 "vcwp Askip Q = (%s.True, Q)" |
49 "vcwp Askip Q = (%s.True, Q)" |