linked_list_rev revisited: replace Coq proofs by lemma functions

examples/linked_list_rev2.mlw

+
+
+(**
+
+{1 In-place linked list reversal }
+
+Version designed for the {h <a href="http://www.lri.fr/~marche/MPRI-2-36-1/">MPRI lecture ``Proof of Programs''</a>}
+
+This is an improved version of {h <a href="linked_list_rev.html">this
+one</a>}: it does not use any Coq proofs, but lemma functions instead.
+
+*)
+
+
+module Disjoint
+
+  use export int.Int
+  use export list.List
+  use export list.Mem
+  use export list.Append
+  use export list.Length
+  use export list.Reverse
+
+  predicate disjoint (l1:list 'a) (l2:list 'a) =
+    forall x:'a. not (mem x l1 /\ mem x l2)
+
+  predicate no_repet (l:list 'a) =
+    match l with
+    | Nil -> true
+    | Cons x r -> not (mem x r) /\ no_repet r
+    end
+
+  let rec ghost mem_decomp (x: 'a) (l: list 'a) : (list 'a, list 'a)
+    requires { mem x l }
+    variant  { l }
+    returns { (l1,l2) -> l = l1 ++ Cons x l2 }
+  = match l with
+    | Nil -> absurd
+    | Cons h t -> if h = x then (Nil,t) else
+       let (r1,r2) = mem_decomp x t in (Cons h r1,r2)
+    end
+
+end
+
+
+
+module InPlaceRev
+
+  use import Disjoint
+  use import map.Map
+  use import ref.Ref
+
+  type loc
+
+  function null:loc
+
+  val acc(field: ref (map loc 'a)) (l:loc) : 'a
+    requires { l <> null }
+    reads { field }
+    ensures { result = get !field l }
+
+  val upd(field: ref (map loc 'a)) (l:loc) (v:'a):unit
+    requires { l <> null }
+    writes { field }
+    ensures { !field = set (old !field) l v }
+
+
+  inductive list_seg loc (map loc loc) (list loc) loc =
+  | list_seg_nil: forall p:loc, next:map loc loc. list_seg p next Nil p
+  | list_seg_cons: forall p q:loc, next:map loc loc, l:list loc.
+      p <> null /\ list_seg (get next p) next l q ->
+         list_seg p next (Cons p l) q
+
+  let rec lemma list_seg_frame_ext (next1 next2:map loc loc)
+    (p q r v: loc) (pM:list loc)
+    requires { list_seg p next1 pM r }
+    requires { next2 = set next1 q v }
+    requires { not (mem q pM) }
+    variant  { pM }
+    ensures  { list_seg p next2 pM r }
+  = match pM with
+    | Nil -> ()
+    | Cons h t ->
+       assert { p = h };
+       list_seg_frame_ext next1 next2 (get next1 p) q r v t
+    end
+
+  let rec lemma list_seg_functional (next:map loc loc) (l1 l2:list loc) (p: loc)
+    requires { list_seg p next l1 null }
+    requires { list_seg p next l2 null }
+    variant  { l1 }
+    ensures  { l1 = l2 }
+  = match l1,l2 with
+    | Nil, Nil -> ()
+    | Cons _ r1, Cons _ r2 -> list_seg_functional next r1 r2 (get next p)
+    | _ -> absurd
+    end
+
+  let rec lemma list_seg_sublistl (next:map loc loc) (l1 l2:list loc) (p q: loc)
+    requires { list_seg p next (l1 ++ Cons q l2) null }
+    variant { l1 }
+    ensures { list_seg q next (Cons q l2) null }
+  = match l1 with
+    | Nil -> ()
+    | Cons _ r -> list_seg_sublistl next r l2 (get next p) q
+    end
+
+  let rec lemma list_seg_no_repet (next:map loc loc) (p: loc) (pM:list loc)
+    requires { list_seg p next pM null }
+    variant  { pM }
+    ensures  { no_repet pM }
+  = match pM with
+    | Nil -> ()
+    | Cons h t ->
+      if mem h t then
+         (* absurd case *)
+         let (l1,l2) = mem_decomp h t in
+         list_seg_sublistl next (Cons h l1) l2 p h;
+         list_seg_functional next pM (Cons h l2) p;
+         assert { length pM > length (Cons h l2) }
+      else
+        list_seg_no_repet next (get next p) t
+    end
+
+  let rec lemma list_seg_append (next:map loc loc) (p q r: loc) (pM qM:list loc)
+    requires { list_seg p next pM q }
+    requires { list_seg q next qM r }
+    variant  { pM }
+    ensures  { list_seg p next (pM ++ qM) r }
+  = match pM with
+    | Nil -> ()
+    | Cons _ t ->
+      list_seg_append next (get next p) q r t qM
+    end
+
+  val next : ref (map loc loc)
+
+  let app (l1 l2:loc) (ghost l1M l2M:list loc) : loc
+    requires { list_seg l1 !next l1M null }
+    requires { list_seg l2 !next l2M null }
+    requires { disjoint l1M l2M }
+    ensures { list_seg result !next (l1M ++ l2M) null }
+  =
+    if l1 = null then l2 else
+    let p = ref l1 in
+    let pM = ref l1M in
+    let l1pM = ref (Nil : list loc) in
+    while acc next !p <> null do
+      invariant { !p <> null }
+      invariant { list_seg l1 !next !l1pM !p }
+      invariant { list_seg !p !next !pM null }
+      invariant { !l1pM ++ !pM = l1M }
+      invariant { disjoint !l1pM !pM }
+      variant   { !pM }
+        l1pM := !l1pM ++ Cons !p Nil;
+        p := acc next !p;
+        match !pM with
+        | Nil -> absurd
+        | Cons _ t -> pM := t
+        end
+    done;
+    upd next !p l2;
+    assert { list_seg l1 !next !l1pM !p };
+    assert { list_seg !p !next (Cons !p Nil) l2 };
+    assert { list_seg l2 !next l2M null };
+    l1
+
+end
+
+
+
+
+
+
+(*
+Local Variables:
+compile-command: "why3 ide linked_list_rev2.mlw"
+End:
+*)

examples/linked_list_rev2/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="4">
+<prover id="0" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
+<prover id="1" name="Z3" version="4.3.1" timelimit="5" memlimit="1000"/>
+<prover id="2" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
+<file name="../linked_list_rev2.mlw" expanded="true">
+<theory name="Disjoint" sum="9c582db93bf8e816b74d113c3748231e" expanded="true">
+ <goal name="WP_parameter mem_decomp" expl="VC for mem_decomp">
+ <proof prover="2"><result status="valid" time="0.02" steps="54"/></proof>
+ </goal>
+</theory>
+<theory name="InPlaceRev" sum="28ff7e317aff1da053e16416b20e10da" expanded="true">
+ <goal name="WP_parameter list_seg_frame_ext" expl="VC for list_seg_frame_ext">
+ <proof prover="2"><result status="valid" time="0.16" steps="278"/></proof>
+ </goal>
+ <goal name="WP_parameter list_seg_functional" expl="VC for list_seg_functional">
+ <proof prover="2"><result status="valid" time="0.10" steps="326"/></proof>
+ </goal>
+ <goal name="WP_parameter list_seg_sublistl" expl="VC for list_seg_sublistl">
+ <proof prover="0"><result status="valid" time="0.29"/></proof>
+ </goal>
+ <goal name="WP_parameter list_seg_no_repet" expl="VC for list_seg_no_repet">
+ <proof prover="2"><result status="valid" time="0.72" steps="241"/></proof>
+ </goal>
+ <goal name="WP_parameter list_seg_append" expl="VC for list_seg_append">
+ <proof prover="2"><result status="valid" time="0.48" steps="712"/></proof>
+ </goal>
+ <goal name="WP_parameter app" expl="VC for app">
+ <transf name="split_goal_wp">
+  <goal name="WP_parameter app.1" expl="1. postcondition">
+  <proof prover="2"><result status="valid" time="0.03" steps="40"/></proof>
+  </goal>
+  <goal name="WP_parameter app.2" expl="2. loop invariant init">
+  <proof prover="2"><result status="valid" time="0.01" steps="4"/></proof>
+  </goal>
+  <goal name="WP_parameter app.3" expl="3. loop invariant init">
+  <proof prover="2"><result status="valid" time="0.02" steps="5"/></proof>
+  </goal>
+  <goal name="WP_parameter app.4" expl="4. loop invariant init">
+  <proof prover="2"><result status="valid" time="0.01" steps="4"/></proof>
+  </goal>
+  <goal name="WP_parameter app.5" expl="5. loop invariant init">
+  <proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
+  </goal>
+  <goal name="WP_parameter app.6" expl="6. loop invariant init">
+  <proof prover="2"><result status="valid" time="0.00" steps="10"/></proof>
+  </goal>
+  <goal name="WP_parameter app.7" expl="7. precondition">
+  <proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
+  </goal>
+  <goal name="WP_parameter app.8" expl="8. precondition">
+  <proof prover="2"><result status="valid" time="0.01" steps="11"/></proof>
+  </goal>
+  <goal name="WP_parameter app.9" expl="9. unreachable point">
+  <proof prover="2"><result status="valid" time="0.06" steps="132"/></proof>
+  </goal>
+  <goal name="WP_parameter app.10" expl="10. loop invariant preservation">
+  <proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
+  </goal>
+  <goal name="WP_parameter app.11" expl="11. loop invariant preservation">
+  <proof prover="1"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="WP_parameter app.12" expl="12. loop invariant preservation">
+  <proof prover="2"><result status="valid" time="0.08" steps="121"/></proof>
+  </goal>
+  <goal name="WP_parameter app.13" expl="13. loop invariant preservation">
+  <proof prover="2"><result status="valid" time="0.22" steps="152"/></proof>
+  </goal>
+  <goal name="WP_parameter app.14" expl="14. loop invariant preservation">
+  <proof prover="2"><result status="valid" time="2.64" steps="614"/></proof>
+  </goal>
+  <goal name="WP_parameter app.15" expl="15. loop variant decrease">
+  <proof prover="2"><result status="valid" time="0.03" steps="43"/></proof>
+  </goal>
+  <goal name="WP_parameter app.16" expl="16. precondition">
+  <proof prover="2"><result status="valid" time="0.02" steps="10"/></proof>
+  </goal>
+  <goal name="WP_parameter app.17" expl="17. assertion">
+  <proof prover="2"><result status="valid" time="0.18" steps="101"/></proof>
+  </goal>
+  <goal name="WP_parameter app.18" expl="18. assertion">
+  <proof prover="2"><result status="valid" time="0.02" steps="23"/></proof>
+  </goal>
+  <goal name="WP_parameter app.19" expl="19. assertion">
+  <proof prover="2"><result status="valid" time="0.67" steps="235"/></proof>
+  </goal>
+  <goal name="WP_parameter app.20" expl="20. postcondition">
+  <proof prover="0"><result status="valid" time="0.22"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>