|
1476
|
1 |
(* Title: HOL/IMP/VC.thy
|
|
1447
|
2 |
ID: $Id$
|
|
1476
|
3 |
Author: Tobias Nipkow
|
|
1447
|
4 |
Copyright 1996 TUM
|
|
|
5 |
|
|
|
6 |
acom: annotated commands
|
|
|
7 |
vc: verification-conditions
|
|
|
8 |
wp: weakest (liberal) precondition
|
|
|
9 |
*)
|
|
|
10 |
|
|
|
11 |
VC = Hoare +
|
|
|
12 |
|
|
|
13 |
datatype acom = Askip
|
|
|
14 |
| Aass loc aexp
|
|
|
15 |
| Asemi acom acom
|
|
|
16 |
| Aif bexp acom acom
|
|
|
17 |
| Awhile bexp assn acom
|
|
|
18 |
|
|
|
19 |
consts
|
|
|
20 |
vc,wp :: acom => assn => assn
|
|
1451
|
21 |
vcwp :: "acom => assn => assn * assn"
|
|
1447
|
22 |
astrip :: acom => com
|
|
|
23 |
|
|
|
24 |
primrec wp acom
|
|
|
25 |
wp_Askip "wp Askip Q = Q"
|
|
|
26 |
wp_Aass "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"
|
|
|
27 |
wp_Asemi "wp (Asemi c d) Q = wp c (wp d Q)"
|
|
|
28 |
wp_Aif "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))"
|
|
|
29 |
wp_Awhile "wp (Awhile b I c) Q = I"
|
|
|
30 |
|
|
|
31 |
primrec vc acom
|
|
|
32 |
vc_Askip "vc Askip Q = (%s.True)"
|
|
|
33 |
vc_Aass "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)"
|
|
|
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) &
|
|
|
37 |
(I s & B b s --> wp c I s) & vc c I s)"
|
|
|
38 |
|
|
|
39 |
primrec astrip acom
|
|
|
40 |
astrip_Askip "astrip Askip = skip"
|
|
|
41 |
astrip_Aass "astrip (Aass x a) = (x:=a)"
|
|
|
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)"
|
|
|
44 |
astrip_Awhile "astrip (Awhile b I c) = whileC b (astrip c)"
|
|
1451
|
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 |
|
|
1447
|
66 |
end
|