Wiki Agenda Contact Version française

In-Place Linked-List Reversal in Why3

This is a Why3 version of the classical example of in-place linked-list reversal


Authors: Claude Marché

Topics: Inductive predicates / List Data Structure / Separation challenges / Ghost code / Pointer Programs

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


In-place linked list reversal

Version designed for the MPRI lecture ``Proof of Programs''

This is an improved version of this one: it does not use any Coq proofs, but lemma functions instead.

module InPlaceRev

  use map.Map
  use ref.Ref
  use int.Int
  use list.List
  use list.Quant as Q
  use list.Append
  use list.Mem
  use list.Length
  use export list.Reverse

  type loc

  val function eq_loc (l1 l2:loc) : bool
    ensures { result <-> l1 = l2 }

  val constant null : loc

  predicate disjoint (l1:list loc) (l2:list loc) =
    forall x:loc. not (mem x l1 /\ mem x l2)

  predicate no_repet (l:list loc) =
    match l with
    | Nil -> true
    | Cons x r -> not (mem x r) /\ no_repet r
    end

  let rec ghost mem_decomp (x: loc) (l: list loc)
    : (l1: list loc, l2: list loc)
    requires { mem x l }
    variant  { l }
    ensures  { l = l1 ++ Cons x l2 }
  = match l with
    | Nil -> absurd
    | Cons h t -> if eq_loc h x then (Nil,t) else
       let (r1,r2) = mem_decomp x t in (Cons h r1,r2)
    end

  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 eq_loc l1 null then l2 else
    let p = ref l1 in
    let ghost pM = ref l1M in
    let ghost l1pM = ref (Nil : list loc) in
    while not (eq_loc (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 }
        match !pM with
        | Nil -> absurd
        | Cons h t ->
          pM := t;
          assert { disjoint !l1pM !pM };
          assert { not (mem h !pM) };
          l1pM := !l1pM ++ Cons h Nil;
        end;
        p := acc next !p
    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

  let in_place_reverse (l:loc) (ghost lM:list loc) : loc
    requires { list_seg l !next lM null }
    ensures  { list_seg result !next (reverse lM) null }
  = let p = ref l in
    let ghost pM = ref lM in
    let r = ref null in
    let ghost rM = ref (Nil : list loc) in
    while not (eq_loc !p null) do
      invariant { list_seg !p !next !pM null }
      invariant { list_seg !r !next !rM null }
      invariant { disjoint !pM !rM }
      invariant { (reverse !pM) ++ !rM = reverse lM }
      variant   { !pM }
      let n = get !next !p in
      upd next !p !r;
      assert { list_seg !r !next !rM null };
      r := !p;
      p := n;
      match !pM with
      | Nil -> absurd
      | Cons h t -> rM := Cons h !rM; pM := t
      end
      done;
    !r

end

Using sequences instead of lists

module InPlaceRevSeq

  use int.Int
  use map.Map as Map
  use seq.Seq
  use seq.Mem
  use seq.Reverse

  type loc

  val function null: loc

  val function eq_loc (l1 l2:loc) : bool
    ensures { result <-> l1 = l2 }

  predicate disjoint (s1: seq 'a) (s2: seq 'a) =
    (* forall x:'a. not (mem x s1 /\ mem x s2) *)
    forall i1. 0 <= i1 < length s1 ->
    forall i2. 0 <= i2 < length s2 ->
    s1[i1] <> s2[i2]

  predicate no_repet (s: seq loc) =
    forall i. 0 <= i < length s -> not (mem s[i] s[i+1..])

  lemma non_empty_seq:
    forall s: seq 'a. length s > 0 ->
    s == cons s[0] s[1..]

  let rec ghost mem_decomp (x: loc) (s: seq loc) : (s1: seq loc, s2: seq loc)
    requires { mem x s }
    variant  { length s }
    ensures  { s == s1 ++ cons x s2 }
  =
    if eq_loc s[0] x then (empty, s[1..])
    else begin
      assert { s == cons s[0] s[1..] };
      let (s1, s2) = mem_decomp x s[1..] in (cons s[0] s1, s2)
    end

  use ref.Ref

  type memory 'a = ref (Map.map loc 'a)

  val acc (field: memory 'a) (l:loc) : 'a
    requires { l <> null }
    reads    { field }
    ensures  { result = Map.get !field l }

  val upd (field: memory 'a) (l: loc) (v: 'a) : unit
    requires { l <> null }
    writes   { field }
    ensures  { !field = Map.set (old !field) l v }

  type next = Map.map loc loc

  predicate list_seg (next: next) (p: loc) (s: seq loc) (q: loc) =
    let n = length s in
    (forall i. 0 <= i < n -> s[i] <> null) /\
    (   (p = q /\ n = 0)
     \/ (1 <= n /\ s[0] = p /\ Map.get next s[n-1] = q /\
         forall i. 0 <= i < n-1 -> Map.get next s[i] = s[i+1]))

  lemma list_seg_frame_ext:
    forall next1 next2: next, p q r v: loc, pM: seq loc.
    list_seg next1 p pM r ->
    next2 = Map.set next1 q v ->
    not (mem q pM) ->
    list_seg next2 p pM r

  let rec lemma list_seg_functional (next: next) (l1 l2: seq loc) (p: loc)
    requires { list_seg next p l1 null }
    requires { list_seg next p l2 null }
    variant  { length l1 }
    ensures  { l1 == l2 }
  = if length l1 > 0 && length l2 > 0 then begin
      assert { l1[0] = l2[0] = p };
      list_seg_functional next l1[1..] l2[1..] (Map.get next p)
    end

  let rec lemma list_seg_tail (next: next) (l1: seq loc) (p q: loc)
    requires { list_seg next p l1 q }
    requires { length l1 > 0 }
    variant  { length l1 }
    ensures  { list_seg next (Map.get next p)l1[1..] q }
  = if length l1 > 1 then
      list_seg_tail next l1[1..] (Map.get next p) q

  let rec lemma list_seg_append (next: next) (p q r: loc) (pM qM: seq loc)
    requires { list_seg next p pM q }
    requires { list_seg next q qM r }
    variant  { length pM }
    ensures  { list_seg next p (pM ++ qM) r }
  =  if length pM > 0 then
      list_seg_append next (Map.get next p) q r pM[1..] qM

  lemma seq_tail_append:
    forall l1 l2: seq 'a.
    length l1 > 0 -> (l1 ++ l2)[1..] == l1[1..] ++ l2

  let rec lemma list_seg_prefix (next: next) (l1 l2: seq loc) (p q: loc)
    requires { list_seg next p (l1 ++ cons q l2) null }
    variant  { length l1 }
    ensures  { list_seg next p l1 q }
  = if length l1 > 0 then begin
      list_seg_tail next (l1 ++ cons q l2) p null;
      list_seg_prefix next l1[1..] l2 (Map.get next p) q
    end

  let rec lemma list_seg_sublistl (next: next) (l1 l2: seq loc) (p q: loc)
    requires { list_seg next p (l1 ++ cons q l2) null }
    variant  { length l1 }
    ensures  { list_seg next q (cons q l2) null }
  = assert { list_seg next p l1 q };
    if length l1 > 0 then begin
      list_seg_tail next l1 p q;
      list_seg_sublistl next l1[1..] l2 (Map.get next p) q
    end

  lemma get_tail:
    forall i: int, s: seq 'a. 0 <= i < length s - 1 -> s[1..][i] = s[i+1]
  lemma tail_suffix:
    forall i: int, s: seq 'a. 0 <= i < length s -> s[1..][i..] == s[i+1..]

  let rec lemma list_seg_no_repet (next: next) (p: loc) (pM: seq loc)
    requires { list_seg next p pM null }
    variant  { length pM }
    ensures  { no_repet pM }
  = if length pM > 0 then begin
      let h = pM[0] in
      let t = pM[1..] in
      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 begin
        assert { not (mem pM[0] pM[0+1..]) };
        list_seg_no_repet next (Map.get next p) t;
        assert { forall i. 1 <= i < length pM -> not (mem pM[i] pM[i+1..]) }
      end
    end

  val next : ref next

  let app (l1 l2: loc) (ghost l1M l2M: seq loc) : loc
    requires { list_seg !next l1 l1M null }
    requires { list_seg !next l2 l2M null }
    requires { disjoint l1M l2M }
    ensures  { list_seg !next result (l1M ++ l2M) null }
  =
    if eq_loc l1 null then l2 else
    let p = ref l1 in
    let ghost pM = ref l1M in
    let ghost l1pM = ref (empty : seq loc) in
    ghost list_seg_no_repet !next l1 l1M;
    while not (eq_loc (acc next !p) null) do
      invariant { !p <> null }
      invariant { list_seg !next l1 !l1pM !p }
      invariant { list_seg !next !p !pM null }
      invariant { !l1pM ++ !pM == l1M }
      invariant { disjoint !l1pM !pM }
      variant   { length !pM }
      assert { length !pM > 0 };
      assert { not (mem !p !l1pM) };
      let ghost t = !pM[1..] in
      ghost l1pM := !l1pM ++ cons !p empty;
      ghost pM := t;
      p := acc next !p
    done;
    upd next !p l2;
    assert { list_seg !next l1 !l1pM !p };
    assert { list_seg !next !p (cons !p empty) l2 };
    assert { list_seg !next l2 l2M null };
    l1

  let in_place_reverse (l:loc) (ghost lM: seq loc) : loc
    requires { list_seg !next l lM null }
    ensures  { list_seg !next result (reverse lM) null }
  = let p = ref l in
    let ghost pM = ref lM in
    let r = ref null in
    let ghost rM = ref (empty: seq loc) in
    while not (eq_loc !p null) do
      invariant { list_seg !next !p !pM null }
      invariant { list_seg !next !r !rM null }
      invariant { disjoint !pM !rM }
      invariant { (reverse !pM) ++ !rM == reverse lM }
      variant   { length !pM }
      let n = acc next !p in
      upd next !p !r;
      assert { list_seg !next !r !rM null };
      r := !p;
      p := n;
      rM := cons !pM[0] !rM;
      pM := !pM[1..]
    done;
    !r

end

(*
Local Variables:
compile-command: "why3 ide linked_list_rev.mlw"
End:
*)

download ZIP archive

Why3 Proof Results for Project "linked_list_rev"

Theory "linked_list_rev.InPlaceRev": fully verified

ObligationsCVC4 1.5Z3 4.5.0
VC null0.01---
VC mem_decomp0.04---
VC list_seg_frame_ext0.07---
VC list_seg_functional0.04---
VC list_seg_sublistl0.06---
VC list_seg_no_repet0.07---
VC list_seg_append0.05---
VC app------
split_goal_right
VC app.00.02---
VC app.10.00---
VC app.20.02---
VC app.30.01---
VC app.40.02---
VC app.50.03---
VC app.60.01---
VC app.70.04---
VC app.80.05---
VC app.90.03---
VC app.100.01---
VC app.110.04---
VC app.120.02---
VC app.13---0.09
VC app.140.04---
VC app.150.04---
VC app.160.05---
VC app.170.01---
VC app.180.05---
VC app.190.04---
VC app.200.05---
VC app.210.04---
VC in_place_reverse------
split_goal_right
VC in_place_reverse.00.01---
VC in_place_reverse.10.02---
VC in_place_reverse.20.03---
VC in_place_reverse.30.02---
VC in_place_reverse.40.01---
VC in_place_reverse.50.05---
VC in_place_reverse.60.03---
VC in_place_reverse.70.04---
VC in_place_reverse.80.05---
VC in_place_reverse.90.04---
VC in_place_reverse.100.08---
VC in_place_reverse.110.02---
VC in_place_reverse.120.02---

Theory "linked_list_rev.InPlaceRevSeq": fully verified

ObligationsAlt-Ergo 1.30Alt-Ergo 2.0.0CVC4 1.4CVC4 1.5Z3 4.5.0Z3 4.6.0
VC null---------0.01------
non_empty_seq------------0.31---
VC mem_decomp------------------
split_goal_right
VC mem_decomp.0---------0.04------
VC mem_decomp.1---------0.04------
VC mem_decomp.2---------0.04------
VC mem_decomp.3---------0.04------
VC mem_decomp.4---------0.05------
VC mem_decomp.50.08---------------
list_seg_frame_ext---------0.04------
VC list_seg_functional------------------
split_goal_right
VC list_seg_functional.0---------0.04------
VC list_seg_functional.1---------0.02------
VC list_seg_functional.2---------0.02------
VC list_seg_functional.3---------0.06------
VC list_seg_functional.40.06---------------
VC list_seg_functional.50.10---------------
VC list_seg_functional.6---------0.06------
VC list_seg_tail------------------
split_goal_right
VC list_seg_tail.0---------0.02------
VC list_seg_tail.1---------0.05------
VC list_seg_tail.20.04---------------
VC list_seg_tail.3---------0.05------
VC list_seg_tail.40.13---------------
VC list_seg_append------------------
split_goal_right
VC list_seg_append.0---------0.02------
VC list_seg_append.1---------0.06------
VC list_seg_append.2---------0.04------
VC list_seg_append.3------------------
inline_goal
VC list_seg_append.3.0------------------
split_goal_right
VC list_seg_append.3.0.0---------0.10------
VC list_seg_append.3.0.1---------0.11------
VC list_seg_append.40.29---------------
seq_tail_append0.03---------------
VC list_seg_prefix------------------
split_goal_right
VC list_seg_prefix.0---------0.03------
VC list_seg_prefix.1---------0.04------
VC list_seg_prefix.2---------0.02------
VC list_seg_prefix.3---------0.07------
VC list_seg_prefix.4------------------
inline_goal
VC list_seg_prefix.4.0------------------
split_goal_right
VC list_seg_prefix.4.0.0---------0.07------
VC list_seg_prefix.4.0.1---------0.10------
VC list_seg_prefix.50.30---------------
VC list_seg_sublistl------------------
split_goal_right
VC list_seg_sublistl.0---------0.02------
VC list_seg_sublistl.1---------0.02------
VC list_seg_sublistl.2---------0.03------
VC list_seg_sublistl.3---------0.02------
VC list_seg_sublistl.4---------0.07------
VC list_seg_sublistl.5---------0.06------
VC list_seg_sublistl.6------------------
introduce_premises
VC list_seg_sublistl.6.0------------------
destruct H
VC list_seg_sublistl.6.0.0------------------
assert (l1 = empty)
VC list_seg_sublistl.6.0.0.0------2.07---------
VC list_seg_sublistl.6.0.0.1------------------
assert (forall l:seq 'a. empty ++ l = l)
VC list_seg_sublistl.6.0.0.1.0------------------
assert (forall l:seq 'a. empty ++ l == l)
VC list_seg_sublistl.6.0.0.1.0.0---0.01------------
VC list_seg_sublistl.6.0.0.1.0.1---------0.04------
VC list_seg_sublistl.6.0.0.1.1---------0.04------
VC list_seg_sublistl.6.0.1---------0.02------
get_tail---------0.06------
tail_suffix0.03---------------
VC list_seg_no_repet------------------
split_goal_right
VC list_seg_no_repet.0---------0.03------
VC list_seg_no_repet.1------------------
introduce_premises
VC list_seg_no_repet.1.0---------0.02------
VC list_seg_no_repet.2---0.56------------
VC list_seg_no_repet.3---------0.03------
VC list_seg_no_repet.4---------0.05------
VC list_seg_no_repet.5---------0.07------
VC list_seg_no_repet.6---------0.02------
VC list_seg_no_repet.7---------0.06------
VC list_seg_no_repet.8---------0.05------
VC list_seg_no_repet.9---------1.73---7.98
VC list_seg_no_repet.10---------0.20------
VC app------------------
split_goal_right
VC app.0---------0.78------
VC app.1---------0.02------
VC app.2---------0.02------
VC app.3---------0.04------
VC app.4---------0.02------
VC app.5---------0.04------
VC app.6---------0.04------
VC app.7---------0.02------
VC app.8---------0.05------
VC app.9---------0.59------
VC app.10---------0.03------
VC app.11---------0.03------
VC app.12---------0.08------
VC app.13---------0.04------
VC app.14------------------
introduce_premises
VC app.14.0------------------
inline_goal
VC app.14.0.0------------------
split_goal_right
VC app.14.0.0.00.03---------------
VC app.14.0.0.10.10---------------
VC app.15---------0.06------
VC app.16---------0.06------
VC app.17---1.22------------
VC app.18---------0.02------
VC app.19---------0.06------
VC app.20---------0.07------
VC app.21------------0.55---
VC app.221.45---------------
VC in_place_reverse------------------
split_goal_right
VC in_place_reverse.0---------0.02------
VC in_place_reverse.1---------0.03------
VC in_place_reverse.2---------0.03------
VC in_place_reverse.3---------0.05------
VC in_place_reverse.4---------0.02------
VC in_place_reverse.5---------0.02------
VC in_place_reverse.6---------0.72------
VC in_place_reverse.7---------0.06------
VC in_place_reverse.8---------0.07------
VC in_place_reverse.9---------0.13------
VC in_place_reverse.10------------------
inline_goal
VC in_place_reverse.10.0------------------
split_goal_right
VC in_place_reverse.10.0.0---------0.08------
VC in_place_reverse.10.0.10.15---------------
VC in_place_reverse.11---------0.37------
VC in_place_reverse.12------------------
introduce_premises
VC in_place_reverse.12.0---16.15------------
VC in_place_reverse.130.29---------------