src/HOL/IMP/VC.thy
changeset 45840 dadd139192d1
parent 45745 3a8bc5623410
child 47818 151d137f1095
equal deleted inserted replaced
45834:9c232d370244 45840:dadd139192d1
     5 subsection "VCG via Weakest Preconditions"
     5 subsection "VCG via Weakest Preconditions"
     6 
     6 
     7 text{* Annotated commands: commands where loops are annotated with
     7 text{* Annotated commands: commands where loops are annotated with
     8 invariants. *}
     8 invariants. *}
     9 
     9 
    10 datatype acom = Askip
    10 datatype acom =
    11               | Aassign vname aexp
    11   ASKIP |
    12               | Asemi   acom acom
    12   Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
    13               | Aif     bexp acom acom
    13   Asemi   acom acom      ("_;/ _"  [60, 61] 60) |
    14               | Awhile  assn bexp acom
    14   Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
       
    15   Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
    15 
    16 
    16 text{* Weakest precondition from annotated commands: *}
    17 text{* Weakest precondition from annotated commands: *}
    17 
    18 
    18 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
    19 fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
    19 "pre Askip Q = Q" |
    20 "pre ASKIP Q = Q" |
    20 "pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" |
    21 "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 (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 "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   (\<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        (\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" |
    25 "pre (Awhile I b c) Q = I"
    26 "pre (Awhile I b c) Q = I"
    26 
    27 
    27 text{* Verification condition: *}
    28 text{* Verification condition: *}
    28 
    29 
    29 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
    30 fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where
    30 "vc Askip Q = (\<lambda>s. True)" |
    31 "vc ASKIP Q = (\<lambda>s. True)" |
    31 "vc (Aassign x a) Q = (\<lambda>s. True)" |
    32 "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 (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 (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 I b c) Q =
    35 "vc (Awhile I b c) Q =
    35   (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and>
    36   (\<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        (I s \<and> bval b s \<longrightarrow> pre c I s) \<and>
    37        vc c I s)"
    38        vc c I s)"
    38 
    39 
    39 text{* Strip annotations: *}
    40 text{* Strip annotations: *}
    40 
    41 
    41 fun astrip :: "acom \<Rightarrow> com" where
    42 fun strip :: "acom \<Rightarrow> com" where
    42 "astrip Askip = SKIP" |
    43 "strip ASKIP = SKIP" |
    43 "astrip (Aassign x a) = (x::=a)" |
    44 "strip (Aassign x a) = (x::=a)" |
    44 "astrip (Asemi c\<^isub>1 c\<^isub>2) = (astrip c\<^isub>1; astrip c\<^isub>2)" |
    45 "strip (Asemi c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip 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 "strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" |
    46 "astrip (Awhile I b c) = (WHILE b DO astrip c)"
    47 "strip (Awhile I b c) = (WHILE b DO strip c)"
    47 
       
    48 
    48 
    49 subsection "Soundness"
    49 subsection "Soundness"
    50 
    50 
    51 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
    51 lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}"
    52 proof(induction c arbitrary: Q)
    52 proof(induction c arbitrary: Q)
    53   case (Awhile I b c)
    53   case (Awhile I b c)
    54   show ?case
    54   show ?case
    55   proof(simp, rule While')
    55   proof(simp, rule While')
    56     from `\<forall>s. vc (Awhile I b c) Q s`
    56     from `\<forall>s. vc (Awhile I b 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
    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
    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])
    59     have "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc])
    60     with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}"
    60     with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip c {I}"
    61       by(rule strengthen_pre)
    61       by(rule strengthen_pre)
    62     show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
    62     show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ)
    63   qed
    63   qed
    64 qed (auto intro: hoare.conseq)
    64 qed (auto intro: hoare.conseq)
    65 
    65 
    66 corollary vc_sound':
    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}"
    67   "(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}"
    68 by (metis strengthen_pre vc_sound)
    68 by (metis strengthen_pre vc_sound)
    69 
    69 
    70 
    70 
    71 subsection "Completeness"
    71 subsection "Completeness"
    72 
    72 
    81 proof(induction c arbitrary: P P')
    81 proof(induction c arbitrary: P P')
    82   case Asemi thus ?case by simp (metis pre_mono)
    82   case Asemi thus ?case by simp (metis pre_mono)
    83 qed simp_all
    83 qed simp_all
    84 
    84 
    85 lemma vc_complete:
    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)"
    86  "\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. strip 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'")
    87   (is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'")
    88 proof (induction rule: hoare.induct)
    88 proof (induction rule: hoare.induct)
    89   case Skip
    89   case Skip
    90   show ?case (is "\<exists>ac. ?C ac")
    90   show ?case (is "\<exists>ac. ?C ac")
    91   proof show "?C Askip" by simp qed
    91   proof show "?C ASKIP" by simp qed
    92 next
    92 next
    93   case (Assign P a x)
    93   case (Assign P a x)
    94   show ?case (is "\<exists>ac. ?C ac")
    94   show ?case (is "\<exists>ac. ?C ac")
    95   proof show "?C(Aassign x a)" by simp qed
    95   proof show "?C(Aassign x a)" by simp qed
    96 next
    96 next
   123 
   123 
   124 
   124 
   125 subsection "An Optimization"
   125 subsection "An Optimization"
   126 
   126 
   127 fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
   127 fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where
   128 "vcpre Askip Q = (\<lambda>s. True, Q)" |
   128 "vcpre ASKIP Q = (\<lambda>s. True, Q)" |
   129 "vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" |
   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 =
   130 "vcpre (Asemi c\<^isub>1 c\<^isub>2) Q =
   131   (let (vc\<^isub>2,wp\<^isub>2) = vcpre 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
   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))" |
   133    in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" |