author | clasohm |
Wed, 29 Nov 1995 17:01:41 +0100 | |
changeset 1374 | 5e407f2a3323 |
parent 972 | e61b058d58d2 |
child 1447 | bc2c0acbbf29 |
permissions | -rw-r--r-- |
936 | 1 |
(* Title: HOL/IMP/Hoare.thy |
938 | 2 |
ID: $Id$ |
936 | 3 |
Author: Tobias Nipkow |
4 |
Copyright 1995 TUM |
|
5 |
||
6 |
Semantic embedding of Hoare logic |
|
7 |
*) |
|
8 |
||
9 |
Hoare = Denotation + |
|
10 |
consts |
|
1374 | 11 |
spec :: [state=>bool,com,state=>bool] => bool |
12 |
(* syntax "@spec" :: [bool,com,bool] => bool *) |
|
939 | 13 |
("{{(1_)}}/ (_)/ {{(1_)}}" 10) |
936 | 14 |
defs |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
939
diff
changeset
|
15 |
spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t" |
936 | 16 |
end |
939 | 17 |
(* Pretty-printing of assertions. |
18 |
Not very helpful as long as programs are not pretty-printed. |
|
19 |
ML |
|
20 |
||
21 |
local open Syntax |
|
22 |
||
23 |
fun is_loc a = let val ch = hd(explode a) |
|
24 |
in ord "A" <= ord ch andalso ord ch <= ord "Z" end; |
|
25 |
||
26 |
fun tr(s$t,i) = tr(s,i)$tr(t,i) |
|
27 |
| tr(Abs(x,T,u),i) = Abs(x,T,tr(u,i+1)) |
|
28 |
| tr(t as Free(a,T),i) = if is_loc a then Bound(i) $ free(a) else t |
|
29 |
| tr(t,_) = t; |
|
30 |
||
31 |
fun cond_tr(p) = Abs("",dummyT,tr(p,0)) |
|
32 |
||
33 |
fun spec_tr[p,c,q] = const"spec" $ cond_tr p $ c $ cond_tr q; |
|
34 |
||
35 |
fun tr'(t as (Bound j $ (u as Free(a,_))),i) = if i=j then u else t |
|
36 |
| tr'(s$t,i) = tr'(s,i)$tr'(t,i) |
|
37 |
| tr'(Abs(x,T,u),i) = Abs(x,T,tr'(u,i+1)) |
|
38 |
| tr'(t,_) = t; |
|
39 |
||
40 |
fun spec_tr'[Abs(_,_,p),c,Abs(_,_,q)] = |
|
41 |
const"@spec" $ tr'(p,0) $ c $ tr'(q,0); |
|
42 |
||
43 |
in |
|
44 |
||
45 |
val parse_translation = [("@spec", spec_tr)]; |
|
46 |
val print_translation = [("spec", spec_tr')]; |
|
47 |
||
48 |
end |
|
49 |
*) |