equal
deleted
inserted
replaced
34 "pre SKIP Q = Q" | |
34 "pre SKIP Q = Q" | |
35 "pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
35 "pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
36 "pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" | |
36 "pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" | |
37 "pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = |
37 "pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = |
38 (\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" | |
38 (\<lambda>s. if bval b s then pre C\<^sub>1 Q s else pre C\<^sub>2 Q s)" | |
39 "pre ({I} WHILE b DO C) Q = (\<lambda>s. EX n. I n s)" |
39 "pre ({I} WHILE b DO C) Q = (\<lambda>s. \<exists>n. I n s)" |
40 |
40 |
41 text\<open>Verification condition:\<close> |
41 text\<open>Verification condition:\<close> |
42 |
42 |
43 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where |
43 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> bool" where |
44 "vc SKIP Q = True" | |
44 "vc SKIP Q = True" | |