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