1335
|
1 |
(* Title: HOL/Hoare/Hoare.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Norbert Galm & Tobias Nipkow
|
|
4 |
Copyright 1995 TUM
|
|
5 |
|
|
6 |
Sugared semantic embedding of Hoare logic.
|
|
7 |
*)
|
|
8 |
|
|
9 |
Hoare = Arith +
|
|
10 |
|
|
11 |
types
|
|
12 |
'a prog (* program syntax *)
|
|
13 |
pvar = "nat" (* encoding of program variables ( < 26! ) *)
|
|
14 |
'a state = "pvar => 'a" (* program state *)
|
|
15 |
'a exp ="'a state => 'a" (* denotation of expressions *)
|
|
16 |
'a bexp = "'a state => bool" (* denotation of boolean expressions *)
|
|
17 |
'a com = "'a state => 'a state => bool" (* denotation of programs *)
|
|
18 |
|
|
19 |
syntax
|
1374
|
20 |
"@Skip" :: 'a prog ("SKIP")
|
|
21 |
"@Assign" :: [id, 'a] => 'a prog ("_ := _")
|
|
22 |
"@Seq" :: ['a prog, 'a prog] => 'a prog ("_;//_" [0,1000] 999)
|
|
23 |
"@If" :: [bool, 'a prog, 'a prog] => 'a prog
|
1335
|
24 |
("IF _//THEN// (_)//ELSE// (_)//END")
|
1374
|
25 |
"@While" :: [bool, bool, 'a prog] => 'a prog
|
1335
|
26 |
("WHILE _//DO {_}// (_)//END")
|
|
27 |
|
1374
|
28 |
"@Spec" :: [bool, 'a prog, bool] => bool ("{_}//_//{_}")
|
1335
|
29 |
|
|
30 |
consts
|
|
31 |
(* semantics *)
|
|
32 |
|
1374
|
33 |
Skip :: 'a com
|
|
34 |
Assign :: [pvar, 'a exp] => 'a com
|
|
35 |
Seq :: ['a com, 'a com] => 'a com
|
|
36 |
Cond :: ['a bexp, 'a com, 'a com] => 'a com
|
|
37 |
While :: ['a bexp, 'a bexp, 'a com] => 'a com
|
|
38 |
Iter :: [nat, 'a bexp, 'a com] => 'a com
|
1335
|
39 |
|
1374
|
40 |
Spec :: ['a bexp, 'a com, 'a bexp] => bool
|
1335
|
41 |
|
|
42 |
defs
|
|
43 |
(* denotational semantics *)
|
|
44 |
|
|
45 |
SkipDef "Skip s s' == (s=s')"
|
|
46 |
AssignDef "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
|
|
47 |
SeqDef "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
|
|
48 |
CondDef "Cond b c c' s s' == (b(s) --> c s s') & (~b s --> c' s s')"
|
|
49 |
WhileDef "While b inv c s s' == ? n. Iter n b c s s'"
|
|
50 |
|
|
51 |
IterDef "Iter n b c == nat_rec n (%s s'.~b(s) & (s=s'))
|
|
52 |
(%n_rec iter_rec.%s s'.b(s) & Seq c iter_rec s s')"
|
|
53 |
|
|
54 |
SpecDef "Spec p c q == !s s'. c s s' --> p s --> q s'"
|
|
55 |
|
|
56 |
end
|
|
57 |
|
|
58 |
ML
|
|
59 |
|
|
60 |
|
|
61 |
(*** term manipulation ***)
|
|
62 |
|
|
63 |
(* name_in_term:bool (name:string,trm:term) bestimmt, ob in trm der Name name als Konstante,
|
|
64 |
freie Var., scheme-Variable oder als Name fuer eine Lambda-Abstraktion vorkommt *)
|
|
65 |
|
|
66 |
fun name_in_term (name,Const (s,t)) =(name=s)
|
|
67 |
| name_in_term (name,Free (s,t)) =(name=s)
|
|
68 |
| name_in_term (name,Var ((s,i),t)) =(name=s ^ makestring i)
|
|
69 |
| name_in_term (name,Abs (s,t,trm)) =(name=s) orelse (name_in_term (name,trm))
|
|
70 |
| name_in_term (name,trm1 $ trm2) =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
|
|
71 |
| name_in_term (_,_) =false;
|
|
72 |
|
|
73 |
(* variant_name:string (name:string,trm:term) liefert einen von name abgewandelten Namen (durch Anhaengen
|
|
74 |
von genuegend vielen "_"), der nicht in trm vorkommt. Im Gegensatz zu variant_abs beruecktsichtigt es
|
|
75 |
auch Namen von scheme-Variablen und von Lambda-Abstraktionen in trm *)
|
|
76 |
|
|
77 |
fun variant_name (name,trm) =if name_in_term (name,trm)
|
|
78 |
then variant_name (name ^ "_",trm)
|
|
79 |
else name;
|
|
80 |
|
|
81 |
(* subst_term:term (von:term,nach:term,trm:term) liefert den Term, der aus
|
|
82 |
trm entsteht, wenn alle Teilterme, die gleich von sind, durch nach ersetzt
|
|
83 |
wurden *)
|
|
84 |
|
|
85 |
fun subst_term (von,nach,Abs (s,t,trm)) =if von=Abs (s,t,trm)
|
|
86 |
then nach
|
|
87 |
else Abs (s,t,subst_term (von,nach,trm))
|
|
88 |
| subst_term (von,nach,trm1 $ trm2) =if von=trm1 $ trm2
|
|
89 |
then nach
|
|
90 |
else subst_term (von,nach,trm1) $ subst_term (von,nach,trm2)
|
|
91 |
| subst_term (von,nach,trm) =if von=trm
|
|
92 |
then nach
|
|
93 |
else trm;
|
|
94 |
|
|
95 |
|
|
96 |
(* Translation between program vars ("a" - "z") and their encoding as
|
|
97 |
natural numbers: "a" <==> 0, "b" <==> Suc(0), ..., "z" <==> 25 *)
|
|
98 |
|
|
99 |
fun is_pvarID s = size s=1 andalso "a"<=s andalso s<="z";
|
|
100 |
|
|
101 |
fun pvarID2pvar s =
|
|
102 |
let fun rest2pvar (i,arg) =
|
|
103 |
if i=0 then arg else rest2pvar(i-1, Syntax.const "Suc" $ arg)
|
|
104 |
in rest2pvar(ord s - ord "a", Syntax.const "0") end;
|
|
105 |
|
|
106 |
fun pvar2pvarID trm =
|
|
107 |
let
|
|
108 |
fun rest2pvarID (Const("0",_),i) =chr (i + ord "a")
|
|
109 |
| rest2pvarID (Const("Suc",_) $ trm,i) =rest2pvarID (trm,i+1)
|
|
110 |
in
|
|
111 |
rest2pvarID (trm,0)
|
|
112 |
end;
|
|
113 |
|
|
114 |
|
|
115 |
(*** parse translations: syntax -> semantics ***)
|
|
116 |
|
|
117 |
(* term_tr:term (name:string,trm:term) ersetzt in trm alle freien Variablen, die eine pvarID
|
|
118 |
darstellen, durch name $ pvarID2pvar(pvarID). Beispiel:
|
|
119 |
bei name="s" und dem Term "a=b & a=X" wird der Term "s(0)=s(Suc(0)) & s(0)=X" geliefert *)
|
|
120 |
|
|
121 |
fun term_tr (name,Free (s,t)) = if is_pvarID s
|
|
122 |
then Syntax.free name $ pvarID2pvar s
|
|
123 |
else Free (s,t)
|
|
124 |
| term_tr (name,Abs (s,t,trm)) = Abs (s,t,term_tr (name,trm))
|
|
125 |
| term_tr (name,trm1 $ trm2) = term_tr (name,trm1) $ term_tr (name,trm2)
|
|
126 |
| term_tr (name,trm) = trm;
|
|
127 |
|
|
128 |
fun bool_tr B =
|
|
129 |
let val name = variant_name("s",B)
|
|
130 |
in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,B))) end;
|
|
131 |
|
|
132 |
fun exp_tr E =
|
|
133 |
let val name = variant_name("s",E)
|
|
134 |
in Abs (name,dummyT,abstract_over (Syntax.free name,term_tr (name,E))) end;
|
|
135 |
|
|
136 |
fun prog_tr (Const ("@Skip",_)) = Syntax.const "Skip"
|
|
137 |
| prog_tr (Const ("@Assign",_) $ Free (V,_) $ E) =
|
|
138 |
if is_pvarID V
|
|
139 |
then Syntax.const "Assign" $ pvarID2pvar V $ exp_tr E
|
|
140 |
else error("Not a valid program variable: " ^ quote V)
|
|
141 |
| prog_tr (Const ("@Seq",_) $ C $ C') =
|
|
142 |
Syntax.const "Seq" $ prog_tr C $ prog_tr C'
|
|
143 |
| prog_tr (Const ("@If",_) $ B $ C $ C') =
|
|
144 |
Syntax.const "Cond" $ bool_tr B $ prog_tr C $ prog_tr C'
|
|
145 |
| prog_tr (Const ("@While",_) $ B $ INV $ C) =
|
|
146 |
Syntax.const "While" $ bool_tr B $ bool_tr INV $ prog_tr C;
|
|
147 |
|
|
148 |
fun spec_tr [P,C,Q] = Syntax.const "Spec" $ bool_tr P $ prog_tr C $ bool_tr Q;
|
|
149 |
|
|
150 |
val parse_translation = [("@Spec",spec_tr)];
|
|
151 |
|
|
152 |
|
|
153 |
(*** print translations: semantics -> syntax ***)
|
|
154 |
|
|
155 |
(* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
|
|
156 |
entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
|
|
157 |
bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)
|
|
158 |
|
|
159 |
fun term_tr' (name,Free (s,t) $ trm) =if name=s
|
|
160 |
then Syntax.free (pvar2pvarID trm)
|
|
161 |
else Free (s,t) $ term_tr' (name,trm)
|
|
162 |
| term_tr' (name,Abs (s,t,trm)) =Abs (s,t,term_tr' (name,trm))
|
|
163 |
| term_tr' (name,trm1 $ trm2) =term_tr' (name,trm1) $ term_tr' (name,trm2)
|
|
164 |
| term_tr' (name,trm) =trm;
|
|
165 |
|
|
166 |
fun bexp_tr' (Abs(_,_,b)) =term_tr' (variant_abs ("s",dummyT,b));
|
|
167 |
|
|
168 |
fun exp_tr' (Abs(_,_,e)) =term_tr' (variant_abs ("s",dummyT,e));
|
|
169 |
|
|
170 |
fun com_tr' (Const ("Skip",_)) =Syntax.const "@Skip"
|
|
171 |
| com_tr' (Const ("Assign",_) $ v $ e) =Syntax.const "@Assign" $ Syntax.free (pvar2pvarID v) $ exp_tr' e
|
|
172 |
| com_tr' (Const ("Seq",_) $ c $ c') =Syntax.const "@Seq" $ com_tr' c $ com_tr' c'
|
|
173 |
| com_tr' (Const ("Cond",_) $ b $ c $ c') =Syntax.const "@If" $ bexp_tr' b $ com_tr' c $ com_tr' c'
|
|
174 |
| com_tr' (Const ("While",_) $ b $ inv $ c) =Syntax.const "@While" $ bexp_tr' b $ bexp_tr' inv $ com_tr' c;
|
|
175 |
|
|
176 |
fun spec_tr' [p,c,q] =Syntax.const "@Spec" $ bexp_tr' p $ com_tr' c $ bexp_tr' q;
|
|
177 |
|
|
178 |
val print_translation =[("Spec",spec_tr')];
|