11376
|
1 |
(* Title: HOL/NanoJava/AxSem.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 2001 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
|
7 |
header "Axiomatic Semantics (Hoare Logic)"
|
|
8 |
|
|
9 |
theory AxSem = State:
|
|
10 |
|
|
11 |
types assn = "state => bool"
|
|
12 |
triple = "assn \<times> stmt \<times> assn"
|
|
13 |
translations
|
|
14 |
"assn" \<leftharpoondown> (type)"state => bool"
|
|
15 |
"triple" \<leftharpoondown> (type)"assn \<times> stmt \<times> assn"
|
|
16 |
|
|
17 |
consts hoare :: "(triple set \<times> triple set) set"
|
|
18 |
syntax (xsymbols)
|
|
19 |
"@hoare" :: "[triple set, triple set ] => bool" ("_ |\<turnstile>/ _" [61,61] 60)
|
|
20 |
"@hoare1" :: "[triple set, assn,stmt,assn] => bool"
|
|
21 |
("_ \<turnstile>/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3]60)
|
|
22 |
syntax
|
|
23 |
"@hoare" :: "[triple set, triple set ] => bool" ("_ ||-/ _" [61,61] 60)
|
|
24 |
"@hoare1" :: "[triple set, assn,stmt,assn] => bool"
|
|
25 |
("_ |-/ ({(1_)}/ (_)/ {(1_)})" [61,3,90,3] 60)
|
|
26 |
|
|
27 |
translations "A |\<turnstile> C" \<rightleftharpoons> "(A,C) \<in> hoare"
|
|
28 |
"A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}"
|
|
29 |
|
|
30 |
inductive hoare
|
|
31 |
intros
|
|
32 |
|
|
33 |
Skip: "A |- {P} Skip {P}"
|
|
34 |
|
|
35 |
Comp: "[| A |- {P} c1 {Q}; A |- {Q} c2 {R} |] ==> A |- {P} c1;;c2 {R}"
|
|
36 |
|
|
37 |
Cond: "[| A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c1 {Q};
|
|
38 |
A |- {\<lambda>s. P s \<and> s<e> = Null} c2 {Q} |] ==>
|
|
39 |
A |- {P} If(e) c1 Else c2 {Q}"
|
|
40 |
|
|
41 |
Loop: "A |- {\<lambda>s. P s \<and> s<e> \<noteq> Null} c {P} ==>
|
|
42 |
A |- {P} While(e) c {\<lambda>s. P s \<and> s<e> = Null}"
|
|
43 |
|
|
44 |
NewC: "A |- {\<lambda>s.\<forall>a. new_Addr s=Addr a--> P (lupd(x|->Addr a)(new_obj a C s))}
|
|
45 |
x:=new C {P}"
|
|
46 |
|
|
47 |
Cast: "A |- {\<lambda>s.(case s<y> of Null=> True | Addr a=> obj_class s a <=C C) -->
|
|
48 |
P (lupd(x|->s<y>) s)} x:=(C)y {P}"
|
|
49 |
|
|
50 |
FAcc: "A |- {\<lambda>s.\<forall>a. s<y>=Addr a-->P(lupd(x|->get_field s a f) s)} x:=y..f{P}"
|
|
51 |
|
|
52 |
FAss: "A |- {\<lambda>s. \<forall>a. s<y>=Addr a --> P (upd_obj a f (s<x>) s)} y..f:=x {P}"
|
|
53 |
|
|
54 |
Call: "\<forall>l. A |- {\<lambda>s'. \<exists>s. P s \<and> l = s \<and>
|
|
55 |
s' = lupd(This|->s<y>)(lupd(Param|->s<p>)(init_locs C m s))}
|
|
56 |
Meth C m {\<lambda>s. Q (lupd(x|->s<Res>)(set_locs l s))} ==>
|
|
57 |
A |- {P} x:={C}y..m(p) {Q}"
|
|
58 |
|
|
59 |
Meth: "\<forall>D. A |- {\<lambda>s. \<exists>a. s<This> = Addr a \<and> D=obj_class s a \<and> D <=C C \<and> P s}
|
|
60 |
Impl D m {Q} ==>
|
|
61 |
A |- {P} Meth C m {Q}"
|
|
62 |
|
|
63 |
(*\<Union>z instead of \<forall>z in the conclusion and
|
|
64 |
z restricted to type state due to limitations of the inductive paackage *)
|
|
65 |
Impl: "A\<union> (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms) ||-
|
|
66 |
(\<Union>z::state. (\<lambda>(C,m). (P z C m, body C m, Q z C m))`ms) ==>
|
|
67 |
A ||- (\<Union>z::state. (\<lambda>(C,m). (P z C m, Impl C m, Q z C m))`ms)"
|
|
68 |
|
|
69 |
(* structural rules *)
|
|
70 |
|
|
71 |
(* z restricted to type state due to limitations of the inductive paackage *)
|
|
72 |
Conseq:"[| \<forall>z::state. A |- {P' z} c {Q' z};
|
|
73 |
\<forall>s t. (\<forall>z::state. P' z s --> Q' z t) --> (P s --> Q t) |] ==>
|
|
74 |
A |- {P} c {Q }"
|
|
75 |
|
|
76 |
Asm: " a \<in> A ==> A ||- {a}"
|
|
77 |
|
|
78 |
ConjI: " \<forall>c \<in> C. A ||- {c} ==> A ||- C"
|
|
79 |
|
|
80 |
ConjE: "[|A ||- C; c \<in> C |] ==> A ||- {c}";
|
|
81 |
|
|
82 |
|
|
83 |
subsection "Derived Rules"
|
|
84 |
|
|
85 |
lemma Conseq1: "\<lbrakk>A \<turnstile> {P'} c {Q}; \<forall>s. P s \<longrightarrow> P' s\<rbrakk> \<Longrightarrow> A \<turnstile> {P} c {Q}"
|
|
86 |
apply (rule hoare.Conseq)
|
|
87 |
apply (rule allI, assumption)
|
|
88 |
apply fast
|
|
89 |
done
|
|
90 |
|
|
91 |
lemma Weaken: "\<lbrakk>A |\<turnstile> C'; C \<subseteq> C'\<rbrakk> \<Longrightarrow> A |\<turnstile> C"
|
|
92 |
apply (rule hoare.ConjI)
|
|
93 |
apply clarify
|
|
94 |
apply (drule hoare.ConjE)
|
|
95 |
apply fast
|
|
96 |
apply assumption
|
|
97 |
done
|
|
98 |
|
|
99 |
lemma Union: "A |\<turnstile> (\<Union>z. C z) = (\<forall>z. A |\<turnstile> C z)"
|
|
100 |
by (auto intro: hoare.ConjI hoare.ConjE)
|
|
101 |
|
|
102 |
lemma Impl':
|
11449
|
103 |
"\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
|
11376
|
104 |
(\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms ==>
|
11449
|
105 |
A ||- (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms"
|
11376
|
106 |
apply (drule Union[THEN iffD2])
|
|
107 |
apply (drule hoare.Impl)
|
|
108 |
apply (drule Union[THEN iffD1])
|
|
109 |
apply (erule spec)
|
|
110 |
done
|
|
111 |
|
|
112 |
lemma Impl1:
|
11449
|
113 |
"\<lbrakk>\<forall>z. A\<union> (\<Union>z. (\<lambda>(C,m). (P z C m, Impl C m, Q (z::state) C m))`ms) ||-
|
11376
|
114 |
(\<lambda>(C,m). (P z C m, body C m, Q (z::state) C m))`ms;
|
11449
|
115 |
(C,m)\<in> ms\<rbrakk> \<Longrightarrow>
|
|
116 |
A |- {P z C m} Impl C m {Q (z::state) C m}"
|
11376
|
117 |
apply (drule Impl')
|
|
118 |
apply (erule Weaken)
|
|
119 |
apply (auto del: image_eqI intro: rev_image_eqI)
|
|
120 |
done
|
|
121 |
|
|
122 |
end
|