equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 Copyright 2001 Technische Universitaet Muenchen |
4 Copyright 2001 Technische Universitaet Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header "Axiomatic Semantics (Hoare Logic)" |
7 header "Axiomatic Semantics" |
8 |
8 |
9 theory AxSem = State: |
9 theory AxSem = State: |
10 |
10 |
11 types assn = "state => bool" |
11 types assn = "state => bool" |
12 vassn = "val => assn" |
12 vassn = "val => assn" |
39 "A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}" |
39 "A \<turnstile> {P}c{Q}" \<rightleftharpoons> "A |\<turnstile> {(P,c,Q)}" |
40 "A |\<turnstile>\<^sub>e t" \<rightleftharpoons> "(A,t) \<in> ehoare" |
40 "A |\<turnstile>\<^sub>e t" \<rightleftharpoons> "(A,t) \<in> ehoare" |
41 "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (* shouldn't be necessary *) |
41 "A |\<turnstile>\<^sub>e (P,e,Q)" \<rightleftharpoons> "(A,P,e,Q) \<in> ehoare" (* shouldn't be necessary *) |
42 "A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)" |
42 "A \<turnstile>\<^sub>e {P}e{Q}" \<rightleftharpoons> "A |\<turnstile>\<^sub>e (P,e,Q)" |
43 |
43 |
|
44 |
|
45 subsection "Hoare Logic Rules" |
44 |
46 |
45 inductive hoare ehoare |
47 inductive hoare ehoare |
46 intros |
48 intros |
47 |
49 |
48 Skip: "A |- {P} Skip {P}" |
50 Skip: "A |- {P} Skip {P}" |
84 Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> |
86 Meth: "\<forall>D. A |- {\<lambda>s'. \<exists>s a. s<This> = Addr a \<and> D = obj_class s a \<and> D <=C C \<and> |
85 P s \<and> s' = init_locs D m s} |
87 P s \<and> s' = init_locs D m s} |
86 Impl (D,m) {Q} ==> |
88 Impl (D,m) {Q} ==> |
87 A |- {P} Meth (C,m) {Q}" |
89 A |- {P} Meth (C,m) {Q}" |
88 |
90 |
89 --{* @{text "\<Union>z"} instead of @{text "\<forall>z"} in the conclusion and |
91 --{* @{text "\<Union>z"} instead of @{text "\<forall>z"} in the conclusion and\\ |
90 z restricted to type state due to limitations of the inductive package *} |
92 z restricted to type state due to limitations of the inductive package *} |
91 Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- |
93 Impl: "\<forall>z::state. A\<union> (\<Union>z. (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms) ||- |
92 (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==> |
94 (\<lambda>Cm. (P z Cm, body Cm, Q z Cm))`Ms ==> |
93 A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms" |
95 A ||- (\<lambda>Cm. (P z Cm, Impl Cm, Q z Cm))`Ms" |
94 |
96 |