Commit 0da5f41e authored by Mário Pereira's avatar Mário Pereira
Browse files

Why3 "bootstrap":

The code in file /src/util/pqueue.ml has been extracted from a Why3 proof,
and is now a correct-by-construction OCaml code. This file depends on the Vector
module, which is also an OCaml implementation extracted from another Why3 proof.
The proofs can be found in /examples/util/

This is the result of Aymeric Walch bachelor internship.
parent a67650db
......@@ -192,7 +192,7 @@ LIB_UTIL = config bigInt util opt lists strings \
hashcons wstdlib exn_printer \
json_base json_parser json_lexer \
debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
cmdline warning sysutil rc plugin bigInt number vector pqueue
LIB_CORE = ident ty term pattern decl coercion theory \
task pretty dterm env trans printer model_parser
......
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(** This module implements a priority queue based on a minimal binary heap.
The heap is implemented as a dynamic array, taken from the module vector. *)
(** This is a contribution by Aymeric Walch. *)
(*@ use Order *)
(*@ use Bag *)
module Make (X: sig
type t
val dummy : t
(*@ function cmp : t -> t -> int *)
(*@ axiom is_pre_order: Order.is_pre_order cmp *)
val compare : t -> t -> int
(*@ r = compare x y
ensures r = cmp x y *)
end) : sig
type elt = X.t
type t
(*@ ephemeral *)
(*@ mutable model bag : X.t bag *)
(*@ invariant card bag <= Sys.max_array_length *)
(*@ predicate mem (x: elt) (h: t) := nb_occ x h.bag > 0 *)
val create : unit -> t
(*@ h = create ()
ensures h.bag = empty_bag *)
val is_empty : t -> bool
(*@ b = is_empty h
ensures b <-> h.bag = empty_bag *)
val size : t -> int
(* x = size h
ensures x = card h.bag *)
(*@ function minimum: t -> elt *)
(*@ predicate is_minimum (x: elt) (h: t) :=
mem x h && forall e. mem e h -> X.cmp x e <= 0 *)
(*@ axiom min_def:
forall h. 0 < card h.bag -> is_minimum (minimum h) h *)
val find_min : t -> elt option
(*@ r = find_min h
ensures match r with
| None -> card h.bag = 0
| Some x -> card h.bag > 0 && x = minimum h *)
exception Empty
val find_min_exn : t -> elt
(*@ x = find_min_exn h
raises Empty -> card h.bag = 0
ensures card h.bag > 0 && x = minimum h *)
val delete_min_exn : t -> unit
(*@ delete_min_exn h
modifies h
raises Empty -> card h.bag = 0 && h.bag = old h.bag
ensures (old h).bag = add (minimum (old h)) h.bag *)
val extract_min_exn : t -> elt
(*@ x = extract_min_exn h
modifies h
raises Empty -> card h.bag = 0 && h.bag = old h.bag
ensures x = minimum (old h)
ensures (old h).bag = add x h.bag *)
val insert : elt -> t -> unit
(*@ insert x h
checks card h.bag < Sys.max_array_length
modifies h
ensures h.bag = add x (old h).bag *)
end
module Impl
use int.Int
use int.ComputerDivision
use int.Div2
use int.NumOf
use bag.Bag
use mach.int.Int63
use mach.int.Refint63
use import Vector.Sig as V (* Module mli de vocal traduit en mlw *)
use seq.Seq
use option.Option
use vocal.Order
use option.Option
use ocaml.Pervasives
use ocaml.Sys
scope Make
scope X
type t
val dummy : t
function cmp (x y: t) : int63
axiom is_pre_order: Order.is_pre_order cmp
val compare (x : t) (y : t) : int63
ensures { result = cmp x y }
end
type elt = X.t
predicate le (x y: elt) = X.cmp x y <= 0
function numocc (a: V.t elt) (c: elt) (l u: int) : int =
numof (fun i -> a.view[i] = c) l u
function numocc' (a : V.t elt) (c: elt) : int =
numocc a c 0 (length a.view)
predicate heap_order (a : V.t elt) = forall i.
(0 < 2*i + 1 < length a.view -> le a.view[i] a.view[2*i + 1]) /\
(0 < 2*i + 2 < length a.view -> le a.view[i] a.view[2*i + 2])
(* éventuellement ici un lemma disant
heap_order a ->
forall i. 0 < i < length a.view -> le a.view[div (i-1) 2] a.view[i] *)
type t = {
a : V.t elt;
ghost mutable bag : bag elt;
}
invariant { length a.view = card bag }
invariant { forall x. numocc' a x = nb_occ x bag }
invariant { heap_order a } (* Heap order is preserved *)
by { a = V.create (Some (0 : int63)) X.dummy; bag = empty_bag }
function minimum (h : t) : elt (* = h.a.view[0] ? *)
axiom min_def: forall h. card h.bag <> 0 -> minimum h = h.a.view[0]
predicate is_minimum (x: elt) (h: t) =
mem x h.bag && forall e. mem e h.bag -> X.cmp x e <= 0
lemma num_exist:
forall h x. numocc' h.a x > 0 ->
exists i. 0 <= i < length h.a.view /\ h.a.view[i] = x
let lemma min_coherent (h: t)
requires { 0 < card h.bag }
ensures { is_minimum (minimum h) h }
= let s = h.a.view in
let n = length s in
let rec lemma ismin (i: int)
requires { 0 <= i < n } variant { i } ensures { le s[0] s[i] }
= if i > 0 then ismin (div (i-1) 2)
in ()
(* Useful lemmas for proving invariants, most of the work will be here *)
predicate substitution (a1 a2: V.t elt) (i : int63) =
length a1.view = length a2.view /\
0 <= i < length a1.view /\
(forall k. 0 <= k < length a1.view -> k <> i -> a1.view[k] = a2.view[k])
lemma sub_occ_1: forall a1 a2 : V.t elt, i : int63, x : elt.
substitution a1 a2 i ->
(x <> a1.view[i] /\ x <> a2.view[i]) ->
numocc' a1 x = numocc' a2 x
lemma sub_occ_2: forall a1 a2 i.
substitution a1 a2 i -> a1.view[i] <> a2.view[i] ->
numocc' a1 a1.view[i]
= numocc' a2 a1.view[i] + 1
lemma sub_occ_3: forall a1 a2 i.
substitution a1 a2 i -> a1.view[i] = a2.view[i] ->
numocc' a1 a1.view[i]
= numocc' a2 a1.view[i]
let lemma sub_order (a1 a2 : V.t elt) (i : int63) =
requires {substitution a1 a2 i}
requires { heap_order a1 }
requires { i > 0 -> X.cmp a1.view[div (i - 1) 2] a2.view[i] <= 0 }
requires { 2*i + 1 < length a1.view -> X.cmp a1.view[2*i + 1] a2.view[i] >= 0 }
requires { 2*i + 2 < length a1.view -> X.cmp a1.view[2*i + 2] a2.view[i] >= 0 }
ensures { heap_order a2 }
()
predicate pop (a1 a2: V.t elt) =
length a2.view = length a1.view - 1 /\
forall i. 0 <= i < length a2.view -> a1.view[i] = a2.view[i]
lemma pop_occ_1: forall a1 a2 x.
pop a1 a2 -> x <> a1.view[length a1.view - 1] ->
numocc' a1 x = numocc' a2 x
(* let lemma pop_occ_1 (a1 a2: V.t elt) (x: elt) *)
(* requires { pop a1 a2 } *)
(* requires { x <> a1.view[length a1.view - 1] } *)
(* ensures { numocc a1 x 0 (length a1.view) *)
(* = numocc a2 x 0 (length a2.view) } *)
(* = assert { numocc a1 x 0 (length (view a2)) *)
(* = numocc a2 x 0 (length (view a2)) } *)
lemma pop_occ_2: forall a1 a2.
pop a1 a2 ->
numocc' a1 a1.view[length a1.view - 1] - 1
= numocc' a2 a1.view[length a1.view - 1]
lemma pop_order: forall a1 a2. pop a1 a2 -> heap_order a1 -> heap_order a2
predicate push (a1 a2 : V.t elt ) =
length a2.view = length a1.view + 1 /\
forall i. 0 <= i < length a1.view -> a1.view[i] = a2.view[i]
let ghost push_occ (a1 a2 : V.t elt) =
requires { push a1 a2 }
ensures { forall x. x <> a2.view[length a2.view - 1] -> numocc' a1 x = numocc' a2 x }
ensures { numocc' a1 a2.view[length a2.view - 1] + 1 = numocc' a2 a2.view[length a2.view - 1] }
()
let ghost push_order (a1 a2 : V.t elt) =
requires { length a1.view > 0 }
requires { push a1 a2 }
requires { le a2.view[div (length a1.view - 1) 2] a2.view[length a1.view] }
requires { heap_order a1 }
ensures { heap_order a2 }
()
lemma same_occ: forall b: bag elt, x a.
x <> a -> nb_occ x (Bag.diff b (Bag.singleton a)) = nb_occ x b
let ghost ancestor (a : V.t elt) (i : int) =
requires { heap_order a }
requires { 0 <= i < length a.view }
ensures { i > 0 -> le a.view[div (i-1) 2] a.view[i] }
()
let ghost children (a : V.t elt) (i : int) =
requires { heap_order a }
requires { 0 <= i < length a.view }
ensures { 2*i+1 < length a.view -> le a.view[i] a.view[2*i+1] }
ensures { 2*i+2 < length a.view -> le a.view[i] a.view[2*i+2] }
()
let ghost trans (a : V.t elt) (i : int) =
requires { 0 <= i < length a.view }
requires { heap_order a }
ensures {i > 0 /\ 2*i+1 < length a.view -> le a.view[div (i-1) 2] a.view[2*i+1] }
ensures {i > 0 /\ 2*i+2 < length a.view -> le a.view[div (i-1) 2] a.view[2*i+2] }
ancestor a i;
children a i;
()
let create () : t
ensures { result.bag = empty_bag }
= { a = V.create (Some (0 : int63)) X.dummy; bag = empty_bag }
let is_empty (h : t) : bool
ensures { result <-> h.bag = empty_bag }
= V.is_empty h.a
let size (h : t) : int63
ensures { result = card h.bag }
= V.length h.a
exception Empty
let find_min_exn (h : t) : elt
raises { Empty -> card h.bag = 0 }
ensures { card h.bag > 0 /\ result = minimum h }
= if V.is_empty h.a then raise Empty;
V.get h.a 0
let find_min (h : t) : option elt
ensures { match result with
| None -> card h.bag = 0
| Some x -> card h.bag > 0 && x = minimum h end }
= if V.is_empty h.a then None else Some (V.get h.a 0)
(* REMARK : some post conditions may need the instantiation of sub_occ_1 *)
let rec move_down (a : V.t elt) (i : int63) (x : elt) : unit
requires { heap_order a }
requires { 0 <= i < length a.view }
requires { i > 0 -> le a.view[div (i - 1) 2] x }
ensures { heap_order a }
ensures { forall e. e <> x -> e <> (old a).view[i] -> numocc' a e = numocc' (old a) e }
ensures { let o = (old a).view[i] in
if x = o then
numocc' a x = numocc' (old a) x
else
numocc' a x = numocc' (old a) x + 1 /\
numocc' a o = numocc' (old a) o - 1 }
ensures { length a.view = length (old a).view } (* Needed for delete min *)
variant { length a.view - i }
= let n = V.length a in
let q = if n=1 then -1 else (n-2)/2 in
if i <= q then begin (* 2i+1 exists *)
let j =
let j = 2 * i + 1 in
if j + 1 < n && X.compare (V.get a (j+1)) (V.get a j) < 0 then j+1 else j in
ancestor a (to_int i);
children a (to_int i);
let olda = pure {a} in
if X.compare (V.get a j) x < 0 then begin
V.set a i (V.get a j);
assert { substitution (old a) a i };
sub_order olda a i;
assert { heap_order a };
move_down a j x
end else begin
V.set a i x;
assert { substitution (old a) a i };
sub_order olda a i
end
end else begin (* 2i+1 outside *)
V.set a i x;
assert { substitution (old a) a i };
end
let extract_min_exn (h : t) : elt
raises { Empty -> card h.bag = 0 /\ h.bag = old h.bag }
ensures { result = minimum (old h) }
ensures { (old h).bag = add result h.bag }
(* Property about order is guaranteed by the invariant *)
= try
let x = V.pop h.a in
let n = V.length h.a in
if n <> 0 then begin
let min = V.get h.a 0 in
assert { min = minimum (old h) };
assert { card (Bag.diff h.bag (Bag.singleton min)) = card h.bag - 1 };
move_down h.a 0 x;
h.bag <- Bag.diff h.bag (Bag.singleton min);
min
end else begin
h.bag <- empty_bag;
x
end
with V.Empty -> raise Empty end
let delete_min_exn (h: t) : unit
raises { Empty -> card h.bag = 0 /\ h.bag = old h.bag }
ensures { (old h).bag = add (minimum (old h)) h.bag }
= let _ = extract_min_exn h in
()
let rec move_up (a : V.t elt) (i : int63) (x : elt)
requires { heap_order a }
requires { 0 <= i < length a.view }
requires { 0 <= 2*i + 1 < length a.view -> le x a.view[2*i + 1] }
requires { 0 <= 2*i + 2 < length a.view -> le x a.view[2*i + 2] }
variant { to_int i }
ensures { heap_order a }
ensures { forall e. e <> (old a).view[i] -> e <> x -> numocc' a e = numocc' (old a) e }
ensures { let o = (old a).view[i] in
if x = o then
numocc' a x = numocc' (old a) x
else
numocc' a x = numocc' (old a) x + 1 /\
numocc' a o = numocc' (old a) o - 1 }
ensures { length a.view = length (old a).view } (* Needed for add *)
= let ghost olda = pure { a } in
if i = 0 then begin
V.set a i x;
assert { substitution olda a i };
sub_order olda a i
end
else begin
let j = (i-1)/2 in
let y = V.get a j in
children a (to_int j);
children a (to_int i);
if X.compare y x > 0 then begin
V.set a i y;
assert { substitution olda a i };
trans olda (to_int i);
sub_order olda a i;
move_up a j x
end
else begin
V.set a i x;
assert { substitution olda a i };
sub_order olda a i
end
end
let insert (x : elt) (h : t) : unit
raises { Invalid_argument -> card h.bag >= Sys.max_array_length }
ensures { h.bag = add x (old h).bag }
= if size h = Sys.max_array_length then raise Invalid_argument;
let n = V.length h.a in
let ghost olda = pure { h.a } in
if n = 0 then
V.push h.a x
else begin
let j = (n-1)/2 in
let y = V.get h.a j in
children h.a (to_int j);
if X.compare y x > 0 then begin
V.push h.a y;
push_order olda h.a;
push_occ olda h.a;
assert { numocc' h.a x = numocc' olda x };
move_up h.a j x
end
else begin
V.push h.a x;
push_occ olda h.a;
push_order olda h.a
end
end;
assert { numocc' h.a x = numocc' olda x + 1 };
h.bag <- add x h.bag;
end
end
module Correct
use Impl
clone PQueue.Sig with
type Make.X.t = Make.X.t,
function Make.X.cmp = Make.X.cmp,
goal Make.X.is_pre_order,
val Make.X.compare = Make.X.compare,
type Make.t = Make.t,
val Make.create = Make.create,
val Make.is_empty = Make.is_empty,
val Make.size = Make.size,
val Make.find_min = Make.find_min,
val Make.find_min_exn = Make.find_min_exn,
val Make.delete_min_exn = Make.delete_min_exn,
val Make.extract_min_exn = Make.extract_min_exn,
val Make.insert = Make.insert,
function Make.minimum = Make.minimum,
goal Make.min_def,
exception Make.Empty = Make.Empty
end
This diff is collapsed.
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2018 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(** Vectors (aka resizable arrays, growing arrays, dynamic arrays, etc.)
This module implements arrays that automatically expand as necessary.
Its implementation uses a traditional array and replaces it with a
larger array when needed (and elements are copied from the old array
to the new one). The current implementation doubles the capacity when
growing the array (and shrinks it whenever the number of elements
comes to one fourth of the capacity).
The unused part of the internal array is filled with a dummy value,
which is user-provided at creation time (and referred to below
as ``the dummy value''). Consequently, vectors do not retain pointers
to values that are not used anymore after a shrinking.
Vectors provide an efficient implementation of stacks, with a
better locality of reference than list-based implementations (such
as standard library {!Stack}). A stack interface is provided,
similar to that of {!Stack} (though {!Vector.push} have arguments
in the other way round). Inserting [n] elements with
{!Vector.push} has overall complexity O(n) i.e. each insertion has
amortized constant time complexity. *)
(*@ use List *)
(*@ use Seq *)
type 'a t
(** The polymorphic type of vectors.
This is a mutable data type. *)
(*@ ephemeral *)
(*@ mutable model view: 'a seq *)
(*@ invariant length view <= Sys.max_array_length *)
(** {2 Operations proper to vectors, or with a different type and/or
semantics than those of module [Array]} *)
val create: ?capacity:int -> dummy:'a -> 'a t
(** [create] returns a fresh vector of length [0].
All the elements of this new vector are initially
physically equal to [dummy] (in the sense of the [==] predicate).
When [capacity] is omitted, it defaults to 0. *)
(*@ a = create ?capacity ~dummy
requires let capacity = match capacity with
| None -> 0 | Some c -> to_int c in
0 <= capacity <= Sys.max_array_length
ensures length a.view = 0 *)
val make: ?dummy:'a -> int -> 'a -> 'a t
(** [make dummy n x] returns a fresh vector of length [n] with all elements
initialized with [x]. If [dummy] is omitted, [x] is also used as a
dummy value for this vector. *)
(*@ a = make ?dummy n x
requires 0 <= n <= Sys.max_array_length
ensures length a.view = n
ensures forall i: integer. 0 <= i < n -> a.view[i] = x *)
val init: dummy:'a -> int -> (int -> 'a) -> 'a t
(** [init n f] returns a fresh vector of length [n],
with element number [i] initialized to the result of [f i].
In other terms, [init n f] tabulates the results of [f]
applied to the integers [0] to [n-1].
Raise [Invalid_argument] if [n < 0] or [n > Sys.max_array_length]. *)
(*@ a = init ~dummy n f
requires 0 <= n <= Sys.max_array_length
ensures length a.view = n
ensures forall i: int. 0 <= i < n -> a.view[i] = f i *)
val resize: 'a t -> int -> unit
(** [resize a n] sets the length of vector [a] to [n].
The elements that are no longer part of the vector, if any, are
internally replaced by the dummy value of vector [a], so that they
can be garbage collected when possible.
Raise [Invalid_argument] if [n < 0] or [n > Sys.max_array_length]. *)
(*@ resize a n
checks 0 <= n <= Sys.max_array_length
modifies a
ensures length a.view = n
ensures forall i. 0 <= i < min (length (old a.view)) n ->
a.view[i] = (old a.view)[i] *)
(** {2 Array interface} *)
val clear: 'a t -> unit
(** Discard all elements from a vector.
This is equivalent to setting the size to 0 with [resize]. *)
(*@ clear a
modifies a
ensures length a.view = 0 *)
val is_empty: 'a t -> bool
(** Return [true] if the given vector is empty, [false] otherwise. *)
(*@ r = is_empty a
ensures r <-> length a.view = 0 *)
val length: 'a t -> int
(** Return the length (number of elements) of the given vector.
Note: the number of memory words occupied by the vector can be larger. *)
(*@ n = length a
ensures n = length a.view *)
val get: 'a t -> int -> 'a
(** [get a n] returns the element number [n] of vector [a].
The first element has number [0]. The last element has number
[length a - 1].
Raise [Invalid_argument "Vector.get"]
if [n] is outside the range [0] to [length a - 1]. *)
(*@ x = get a i
requires 0 <= i < length a.view
ensures x = a.view[i] *)
val set: 'a t -> int -> 'a -> unit
(** [set a n x] modifies aector [a] in place, replacing
element number [n] with [x].
Raise [Invalid_argument "Vector.set"]
if [n] is outside the range 0 to [length a - 1]. *)
(*@ set a i x
requires 0 <= i < length a.view
modifies a
ensures length a.view = length (old a).view
ensures a.view[i] = x
ensures forall j. 0 <= j < length a.view -> j <> i ->
a.view[j] = (old a).view[j] *)
val sub: 'a t -> int -> int -> 'a t
(** [sub a start len] returns a fresh vector of length [len], containing
the elements number [start] to [start + len - 1] of vector [a]. *)
(*@ r = sub a ofs n
requires 0 <= ofs /\ 0 <= n /\ ofs + n <= length a.view
ensures length r.view = n
ensures forall i. 0 <= i < n -> r.view[i] = a.view[ofs + i] *)
val fill : 'a t -> int -> int -> 'a -> unit
(** [fill a ofs len x] modifies the vector [a] in place,
storing [x] in elements number [ofs] to [ofs + len - 1].
Raise [Invalid_argument "Vector.fill"] if [ofs] and [len] do not
designate a valid subvector of [a]. *)
(*@ fill a ofs n x
requires 0 <= ofs /\ 0 <= n /\ ofs + n <= length a.view
modifies a
ensures forall i. (0 <= i < ofs \/ ofs + n <= i < length a.view) ->
a.view[i] = (old a).view[i]
ensures forall i. ofs <= i < ofs + n -> a.view[i] = x *)
val blit : 'a t -> int -> 'a t -> int -> int -> unit
(** [blit a1 o1 a2 o2 len] copies [len] elements
from vector [a1], starting at element number [o1], to vector [a2],
starting at element number [o2]. It works correctly even if
[a1] and [a2] are the same vector, and the source and
destination chunks overlap.
Raise [Invalid_argument "Vector.blit"] if [o1] and [len] do not
designate a valid subvector of [a1], or if [o2] and [len] do not
designate a valid subvector of [a2]. *)
(*@ blit a1 ofs1 a2 ofs2 n
requires 0 <= n