equal
deleted
inserted
replaced
8 |
8 |
9 type_synonym assn = "state \<Rightarrow> bool" |
9 type_synonym assn = "state \<Rightarrow> bool" |
10 |
10 |
11 definition |
11 definition |
12 hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where |
12 hoare_valid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<Turnstile> {(1_)}/ (_)/ {(1_)}" 50) where |
13 "\<Turnstile> {P}c{Q} = (\<forall>s t. (c,s) \<Rightarrow> t \<longrightarrow> P s \<longrightarrow> Q t)" |
13 "\<Turnstile> {P}c{Q} = (\<forall>s t. P s \<and> (c,s) \<Rightarrow> t \<longrightarrow> Q t)" |
14 |
14 |
15 abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state" |
15 abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state" |
16 ("_[_'/_]" [1000,0,0] 999) |
16 ("_[_'/_]" [1000,0,0] 999) |
17 where "s[a/x] == s(x := aval a s)" |
17 where "s[a/x] == s(x := aval a s)" |
18 |
18 |