Hoare logic: while rule

examples/hoare_logic/imp.why

@@ -225,6 +225,11 @@ lemma if_rule:
   valid_triple (Fand p (Fnot (Fterm e))) i2 q ->
   valid_triple p (Sif e i1 i2) q
 
+lemma while_rule:
+  forall e:expr, inv:fmla, i:stmt.
+  valid_triple (Fand (Fterm e) inv) i inv ->
+  valid_triple inv (Swhile e i) (Fand (Fnot (Fterm e)) inv)
+
 end
 
 

examples/hoare_logic/imp/why3session.xml

@@ -52,11 +52,11 @@
   version="2.19"/>
  <file
   name="../imp.why"
-  verified="true"
+  verified="false"
   expanded="true">
   <theory
    name="Imp"
-   verified="true"
+   verified="false"
    expanded="true">
    <goal
     name="ident_eq_dec"
@@ -401,6 +401,41 @@
      <result status="valid" time="0.51"/>
     </proof>
    </goal>
+   <goal
+    name="while_rule"
+    sum="94fbdb08982a09191521520728619166"
+    proved="false"
+    expanded="true"
+    shape="avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
+    <proof
+     prover="coq"
+     timelimit="3"
+     edited="imp_Imp_while_rule_1.v"
+     obsolete="true"><undone/>
+     
+    </proof>
+    <proof
+     prover="cvc3"
+     timelimit="3"
+     edited=""
+     obsolete="false">
+     <result status="timeout" time="3.09"/>
+    </proof>
+    <proof
+     prover="alt-ergo"
+     timelimit="3"
+     edited=""
+     obsolete="false">
+     <result status="timeout" time="3.09"/>
+    </proof>
+    <proof
+     prover="z3"
+     timelimit="3"
+     edited=""
+     obsolete="false">
+     <result status="timeout" time="3.09"/>
+    </proof>
+   </goal>
   </theory>
  </file>
 </why3session>