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

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 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 ghost pM = ref l1M in
    let ghost 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 }
        match !pM with
        | Nil -> absurd
        | Cons _ t ->
          l1pM := !l1pM ++ Cons !p Nil;
          pM := t
        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 }
  = 'Init:
    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 !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
      next := set !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 import int.Int
  use map.Map
  use import seq.Seq
  use import seq.Reverse
  use import ref.Ref

  predicate mem (x: 'a) (s: seq 'a) =
    exists i. 0 <= i < length s /\ s[i] = x

  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 'a) =
    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: 'a) (s: seq 'a) : (seq 'a, seq 'a)
    requires { mem x s }
    variant  { length s }
    returns  { (s1,s2) -> s == s1 ++ cons x s2 }
  =
    if 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

  type loc

  function null: loc

  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 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 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 t = !pM[ 1 .. ] in
      l1pM := !l1pM ++ cons !p empty;
      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 }
  = 'Init:
    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 !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.Disjoint": fully verified in 0.02 s

ObligationsAlt-Ergo (0.99.1)
VC for mem_decomp0.02

Theory "linked_list_rev.InPlaceRev": fully verified in 3.35 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)Z3 (4.3.2)
VC for list_seg_frame_ext0.16------
VC for list_seg_functional0.10------
VC for list_seg_sublistl---0.28---
VC for list_seg_no_repet0.05------
VC for list_seg_append0.23------
VC for app---------
split_goal_wp
  1. postcondition0.03------
2. loop invariant init0.01------
3. loop invariant init0.02------
4. loop invariant init0.01------
5. loop invariant init0.01------
6. loop invariant init0.00------
7. precondition0.01------
8. unreachable point0.06------
9. precondition0.01------
10. loop invariant preservation0.01------
11. loop invariant preservation------0.02
12. loop invariant preservation0.08------
13. loop invariant preservation0.06------
14. loop invariant preservation0.32------
15. loop variant decrease0.03------
16. precondition0.02------
17. assertion0.01------
18. assertion0.02------
19. assertion0.32------
20. postcondition---0.23---
VC for in_place_reverse---------
split_goal_wp
  1. loop invariant init0.01------
2. loop invariant init0.02------
3. loop invariant init0.01------
4. loop invariant init0.01------
5. assertion0.09------
6. unreachable point0.05------
7. loop invariant preservation0.30------
8. loop invariant preservation0.11------
9. loop invariant preservation0.56------
10. loop invariant preservation0.01------
11. loop variant decrease0.02------
12. postcondition0.06------

Theory "linked_list_rev.InPlaceRevSeq": fully verified in 71.05 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.4)Z3 (4.3.2)Z3 (4.4.0)
non_empty_seq0.02---------
VC for mem_decomp------------
split_goal_wp
  1. postcondition0.02---------
2. assertion0.00---------
3. variant decrease0.01---------
4. precondition---------0.05
5. postcondition0.12---------
list_seg_frame_ext0.02---------
VC for list_seg_functional------------
split_goal_wp
  1. assertion0.02---------
2. variant decrease0.01------0.01
3. precondition0.15---------
4. precondition0.16------1.95
5. postcondition------0.02---
6. postcondition0.02---------
VC for list_seg_tail------------
split_goal_wp
  1. variant decrease0.01---------
2. precondition0.08---------
3. precondition0.03---------
4. postcondition0.02---------
5. postcondition0.04---------
VC for list_seg_append------------
split_goal_wp
  1. variant decrease0.01---0.03---
2. precondition0.01---0.02---
3. precondition0.01---0.02---
4. postcondition------------
inline_goal
  1. postcondition------------
split_goal_wp
  1. postcondition------4.58---
2. postcondition------2.86---
5. postcondition0.09---0.94---
seq_tail_append0.05---------
VC for list_seg_prefix------------
split_goal_wp
  1. precondition0.03---------
2. precondition0.02---------
3. variant decrease0.06---------
4. precondition0.05---------
5. postcondition------------
inline_goal
  1. postcondition------------
split_goal_wp
  1. postcondition---------0.33
2. postcondition---------0.45
6. postcondition0.98---0.02---
VC for list_seg_sublistl------------
split_goal_wp
  1. assertion0.02---------
2. precondition0.02---------
3. precondition0.03---------
4. variant decrease0.14---------
5. precondition0.03---0.02---
6. postcondition0.02---------
7. postcondition0.36---------
get_tail0.03---------
tail_suffix0.03---------
VC for list_seg_no_repet------------
split_goal_wp
  1. precondition0.02---------
2. precondition------------
introduce_premises
  1. precondition---0.12------
3. precondition0.01---------
4. precondition0.02---------
5. assertion0.11---------
6. postcondition0.02---------
7. assertion0.02---------
8. variant decrease0.04---------
9. precondition0.02---------
10. assertion------------
inline_trivial
  1. assertion------------
inline_goal
  1. assertion------0.04---
11. postcondition0.03---------
12. postcondition0.03---------
VC for app------------
split_goal_wp
  1. postcondition0.04---------
2. precondition0.02---------
3. loop invariant init0.03---------
4. loop invariant init0.03---------
5. loop invariant init0.01---------
6. loop invariant init0.01---------
7. loop invariant init0.02---------
8. precondition0.02---------
9. assertion0.02---------
10. assertion0.01---------
11. precondition0.02---------
12. loop invariant preservation0.02---------
13. loop invariant preservation---------3.12
14. loop invariant preservation0.02---------
15. loop invariant preservation------------
introduce_premises
  1. loop invariant preservation------------
inline_goal
  1. loop invariant preservation------------
split_goal_wp
  1. VC for app0.09---------
2. VC for app------2.66---
16. loop invariant preservation---6.21------
17. loop variant decrease0.85---0.02---
18. precondition0.02---0.01---
19. assertion0.21---0.02---
20. assertion8.12---0.67---
21. assertion------0.08---
22. postcondition---------4.58
VC for in_place_reverse------------
split_goal_wp
  1. loop invariant init0.01---------
2. loop invariant init0.02---------
3. loop invariant init0.02---------
4. loop invariant init0.02---------
5. precondition0.02---------
6. precondition0.02---------
7. assertion0.08---------
8. loop invariant preservation4.50---------
9. loop invariant preservation---------11.12
10. loop invariant preservation------0.51---
11. loop invariant preservation------------
inline_goal
  1. loop invariant preservation------------
split_goal_wp
  1. VC for in_place_reverse0.07---------
2. VC for in_place_reverse12.39---------
12. loop variant decrease0.41---------
13. postcondition0.43---------