equal
deleted
inserted
replaced
8 |
8 |
9 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
9 definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" |
10 ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
10 ("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where |
11 "\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
11 "\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" |
12 |
12 |
13 text{* Proveability of Hoare triples in the proof system for total |
13 text{* Provability of Hoare triples in the proof system for total |
14 correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined |
14 correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined |
15 inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for |
15 inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for |
16 @{text"\<turnstile>"} only in the one place where nontermination can arise: the |
16 @{text"\<turnstile>"} only in the one place where nontermination can arise: the |
17 @{term While}-rule. *} |
17 @{term While}-rule. *} |
18 |
18 |