Hoare logic: total correctness

examples/hoare_logic/wp_total.mlw

@@ -268,14 +268,23 @@ lemma many_steps_seq:
 
 predicate valid_fmla (p:fmla) = forall s:state. eval_fmla s p
 
-(* Hoare triples *)
+(*** Hoare triples ***)
 
+(* partial correctness *)
 predicate valid_triple (p:fmla) (i:stmt) (q:fmla) =
     forall s:state. eval_fmla s p ->
       forall s':state, n:int. many_steps s i s' Sskip n ->
         eval_fmla s' q
 
-(* Hoare logic rules *)
+(* total correctness *)
+(*
+predicate total_valid_triple (p:fmla) (i:stmt) (q:fmla) =
+    forall s:state. eval_fmla s p ->
+      exists s':state, n:int. many_steps s i s' Sskip n /\
+        eval_fmla s' q
+*)
+
+(* Hoare logic rules (partial correctness) *)
 
 lemma skip_rule:
   forall q:fmla. valid_triple q Sskip q
@@ -321,11 +330,25 @@ lemma consequence_rule:
   valid_fmla (Fimplies q q') ->
   valid_triple p' i q'
 
+(* frame rule *)
 
+use set.Set
 
-end
+predicate assigns (s:state) (a:Set.set ident) (s':state) =
+  forall i:ident. not (Set.mem i a) ->
+    eval_term s (Tderef i) = eval_term s' (Tderef i)
 
+function stmt_writes (s:stmt) : Set.set ident =
+  match s with
+  | Sskip -> Set.empty
+  | Sassign i _ -> Set.singleton i
+  | Sseq s1 s2 -> Set.union (stmt_writes s1) (stmt_writes s2)
+  | Sif _ s1 s2 -> Set.union (stmt_writes s1) (stmt_writes s2)
+  | Swhile _ _ s -> stmt_writes s
+  | Sassert _ -> Set.empty
+  end
 
+end
 
 
 module WP
@@ -346,7 +369,7 @@ module WP
         Fand (Fimplies (Fterm e) (wp i1 q))
              (Fimplies (Fnot (Fterm e)) (wp i2 q))
     | Sassert f ->
-       Fimplies f q (* liberal wp, no termination requires *)
+       Fimplies f q (* liberal wp, no termination required *)
        (* Fand f q *) (* strict wp, termination required *)
     | Swhile e inv i ->
         Fand inv

examples/hoare_logic/wp_total/why3session.xml

@@ -363,7 +363,7 @@
    <goal
     name="WP_parameter wp"
     expl="parameter wp"
-    sum="fcf6c0443719c76bb3dd7ad8e2f3d53e"
+    sum="591df36e691adb32904ed88ae9a90b30"
     proved="false"
     expanded="true"
     shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V11aFimpliesaFnotaFtermV8V12V0V1Iavalid_tripleV12V10V1FIavalid_tripleV11V9V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FFF">
@@ -381,7 +381,7 @@
      <goal
       name="WP_parameter wp.1"
       expl="parameter wp"
-      sum="e39ef2792789f35bc7b90f25ed79b298"
+      sum="9728c928640f5dffc1acb5b3e5aadfa9"
       proved="true"
       expanded="false"
       shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
@@ -390,13 +390,13 @@
        timelimit="5"
        edited=""
        obsolete="false">
-       <result status="valid" time="0.05"/>
+       <result status="valid" time="0.04"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter wp.2"
       expl="parameter wp"
-      sum="35730568229c8ac688137a37e2315371"
+      sum="874dd66b46d901159ea98b68e37a8087"
       proved="true"
       expanded="false"
       shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtFF">
@@ -411,7 +411,7 @@
      <goal
       name="WP_parameter wp.3"
       expl="parameter wp"
-      sum="f2d2133eb159207f51a4abc3674e7ac4"
+      sum="7dc89b7a7c368fa12c31491f66aea32a"
       proved="true"
       expanded="false"
       shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSassertVtaSwhileVVVtFF">
@@ -426,7 +426,7 @@
      <goal
       name="WP_parameter wp.4"
       expl="parameter wp"
-      sum="95a4085929243ddade16b291fe90bb0f"
+      sum="e54dfcf53037fdb501243d9bb9f32141"
       proved="true"
       expanded="false"
       shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V9aFimpliesaFnotaFtermV6V10V0V1Iavalid_tripleV10V8V1FIavalid_tripleV9V7V1FaSassertVtaSwhileVVVtFF">
@@ -449,13 +449,13 @@
        timelimit="5"
        edited=""
        obsolete="false">
-       <result status="valid" time="0.66"/>
+       <result status="valid" time="0.62"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter wp.5"
       expl="parameter wp"
-      sum="452220572080dad57c9a7e32b60ffdcb"
+      sum="340770b9524faac64481d3f5e1251b42"
       proved="true"
       expanded="true"
       shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtFF">
@@ -485,13 +485,13 @@
        timelimit="5"
        edited=""
        obsolete="false">
-       <result status="valid" time="0.05"/>
+       <result status="valid" time="0.06"/>
       </proof>
      </goal>
      <goal
       name="WP_parameter wp.6"
       expl="parameter wp"
-      sum="457c7d860257e025ced48c9fdd71eee2"
+      sum="466f38f8e739dc43f0e2e992def28abc"
       proved="false"
       expanded="true"
       shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1V0V1Iavalid_tripleV13V12V11FFF">

src/ide/replay.ml

@@ -141,7 +141,7 @@ module M = Session.Make
          | Some _ -> failwith "Replay.timeout: already one handler installed"
 
      let notify_timer_state w s r =
-       Printf.eprintf "Progress: %d/%d/%d   \r%!" w s r
+       Printf.eprintf "Progress: %d/%d/%d                       \r%!" w s r
 
    end)