src/HOL/IMP/VC.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45212 e87feee00a4c
child 45745 3a8bc5623410
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 header "Verification Conditions"
     2 
     3 theory VC imports Hoare begin
     4 
     5 subsection "VCG via Weakest Preconditions"
     6 
     7 text{* Annotated commands: commands where loops are annotated with
     8 invariants. *}
     9 
    10 datatype acom = Askip
    11               | Aassign vname aexp
    12               | Asemi   acom acom
    13               | Aif     bexp acom acom
    14               | Awhile  bexp assn acom
    15 
    16 text{* Weakest precondition from annotated commands: *}
    17 
    18 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
    19 "pre Askip Q = Q" |
    20 "pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
    21 "pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" |
    22 "pre (Aif b c\<^isub>1 c\<^isub>2) Q =
    23   (\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and>
    24        (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
    25 "pre (Awhile b I c) Q = I"
    26 
    27 text{* Verification condition: *}
    28 
    29 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
    30 "vc Askip Q = (\<lambda>s. True)" |
    31 "vc (Aassign x a) Q = (\<lambda>s. True)" |
    32 "vc (Asemi c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" |
    33 "vc (Aif b c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" |
    34 "vc (Awhile b I c) Q =
    35   (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
    36        (I s \<and> bval b s \<longrightarrow> pre c I s) \<and>
    37        vc c I s)"
    38 
    39 text{* Strip annotations: *}
    40 
    41 fun astrip :: "acom \<Rightarrow> com" where
    42 "astrip Askip = SKIP" |
    43 "astrip (Aassign x a) = (x::=a)" |
    44 "astrip (Asemi c\<^isub>1 c\<^isub>2) = (astrip c\<^isub>1; astrip c\<^isub>2)" |
    45 "astrip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN astrip c\<^isub>1 ELSE astrip c\<^isub>2)" |
    46 "astrip (Awhile b I c) = (WHILE b DO astrip c)"
    47 
    48 
    49 subsection "Soundness"
    50 
    51 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
    52 proof(induction c arbitrary: Q)
    53   case (Awhile b I c)
    54   show ?case
    55   proof(simp, rule While')
    56     from `\<forall>s. vc (Awhile b I c) Q s`
    57     have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and
    58          pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all
    59     have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc])
    60     with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
    61       by(rule strengthen_pre)
    62     show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
    63   qed
    64 qed (auto intro: hoare.conseq)
    65 
    66 corollary vc_sound':
    67   "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} astrip c {Q}"
    68 by (metis strengthen_pre vc_sound)
    69 
    70 
    71 subsection "Completeness"
    72 
    73 lemma pre_mono:
    74   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s"
    75 proof (induction c arbitrary: P P' s)
    76   case Asemi thus ?case by simp metis
    77 qed simp_all
    78 
    79 lemma vc_mono:
    80   "\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s"
    81 proof(induction c arbitrary: P P')
    82   case Asemi thus ?case by simp (metis pre_mono)
    83 qed simp_all
    84 
    85 lemma vc_complete:
    86  "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)"
    87   (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
    88 proof (induction rule: hoare.induct)
    89   case Skip
    90   show ?case (is "\<exists>ac. ?C ac")
    91   proof show "?C Askip" by simp qed
    92 next
    93   case (Assign P a x)
    94   show ?case (is "\<exists>ac. ?C ac")
    95   proof show "?C(Aassign x a)" by simp qed
    96 next
    97   case (Semi P c1 Q c2 R)
    98   from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast
    99   from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast
   100   show ?case (is "\<exists>ac. ?C ac")
   101   proof
   102     show "?C(Asemi ac1 ac2)"
   103       using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
   104   qed
   105 next
   106   case (If P b c1 Q c2)
   107   from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
   108     by blast
   109   from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
   110     by blast
   111   show ?case (is "\<exists>ac. ?C ac")
   112   proof
   113     show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp
   114   qed
   115 next
   116   case (While P b c)
   117   from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
   118   show ?case (is "\<exists>ac. ?C ac")
   119   proof show "?C(Awhile b P ac)" using ih by simp qed
   120 next
   121   case conseq thus ?case by(fast elim!: pre_mono vc_mono)
   122 qed
   123 
   124 
   125 subsection "An Optimization"
   126 
   127 fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
   128 "vcpre Askip Q = (\<lambda>s. True, Q)" |
   129 "vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
   130 "vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
   131   (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
   132        (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2
   133    in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |
   134 "vcpre (Aif b c\<^isub>1 c\<^isub>2) Q =
   135   (let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q;
   136        (vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 Q
   137    in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, \<lambda>s. (bval b s \<longrightarrow> wp\<^isub>1 s) \<and> (\<not>bval b s \<longrightarrow> wp\<^isub>2 s)))" |
   138 "vcpre (Awhile b I c) Q =
   139   (let (vcc,wpc) = vcpre c I
   140    in (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
   141            (I s \<and> bval b s \<longrightarrow> wpc s) \<and> vcc s, I))"
   142 
   143 lemma vcpre_vc_pre: "vcpre c Q = (vc c Q, pre c Q)"
   144 by (induct c arbitrary: Q) (simp_all add: Let_def)
   145 
   146 end