Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

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

Tools: Why3

index



(*

In-place linked list reversal.

Version designed for the MPRI lecture http://www.lri.fr/~marche/MPRI-2-36-1/

*)

theory ListReverse

  use export int.Int
  use export list.List

  function head (l: list 'a) : 'a
  axiom head_cons: forall x:'a, l:list 'a. head (Cons x l) = x
  function tail (l: list 'a) : list 'a
  axiom tail_cons: forall x:'a, l:list 'a. tail (Cons x l) = l

  use export list.Mem

  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

  use export list.Append
  use export list.Reverse

end

module InPlaceRev

  use import ListReverse
  use import map.Map

  type loc

  function null:loc

  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


  lemma list_seg_frame:
    forall next1 next2:map loc loc, p q v: loc, pM:list loc.
      list_seg p next1 pM null /\ next2 = set next1 q v /\
      not (mem q pM) -> list_seg p next2 pM null

  lemma list_seg_functional:
    forall next:map loc loc, l1 l2:list loc, p: loc.
      list_seg p next l1 null /\ list_seg p next l2 null -> l1 = l2

  lemma list_seg_sublistl:
    forall next:map loc loc, l1 l2:list loc, p q: loc.
      list_seg p next (l1++Cons q l2) null ->
        list_seg q next (Cons q l2) null

  lemma list_seg_no_repet:
    forall next:map loc loc, pM:list loc, p: loc.
      list_seg p next pM null -> no_repet pM

  use import module ref.Ref

  val next : ref (map loc loc)

  let in_place_reverse (l:loc) (lM:list loc) : loc =
    { list_seg l !next lM null }
    'Init:
    let p = ref l in
    let pM = ref lM in
    let r = ref null in
    let rM = ref (Nil : list loc) in
    while !p <> null do
      invariant {
         list_seg !p !next !pM null /\
         list_seg !r !next !rM null /\
         disjoint !pM !rM /\
         (reverse !pM) ++ !rM = reverse lM
        }
        let n = get !next !p in
        next := set !next !p !r;
        assert { list_seg !r !next !rM null };
        r := !p;
        p := n;
        rM := Cons (head !pM) !rM;
        pM := tail !pM
    done;
    !r
    { list_seg result !next (reverse lM) null }

end


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