Commit 7bb00702 authored by MARCHE Claude's avatar MARCHE Claude

Vacid0 Binary Heaps: abstraction, heapSort and test harness

parent 1813aa31
......@@ -144,6 +144,7 @@ why3.conf
/tests/test-jcf/
/tests/test-pgm-jcf/
/tests/test-claude/
/tests/test-and/
# /examples/
/examples/genealogy/
......
module AbstractHeap
(**** logic declarations *****)
use import int.Int
use import bag.Bag
use import bag_of_integers.Bag_integers
(* abstract interface for heaps *)
type logic_heap
function model (h:logic_heap): (bag int)
use import module ref.Ref
val create :
sz:int ->
{ 0 <= sz }
ref logic_heap
{ model !result = empty_bag }
val insert :
this:ref logic_heap -> e:int ->
{ true }
unit writes this
{ model !this = add e (model (old !this)) }
val extractMin :
this:ref logic_heap ->
{ model !this <> empty_bag }
int writes this
{ result = min_bag (model (old !this)) /\
model (old !this) = add result (model !this) /\
card (model (old !this)) = (card (model !this)) + 1
}
end
(*
Local Variables:
compile-command: "why3ide -I . proofs"
End:
*)
theory Bag
use import int.Int
use import map.Map as A
type bag 'a = A.map 'a int
(* the most basic operation is the number of occurences *)
function nb_occ (x: 'a) (b: bag 'a): int = A.get b x
axiom occ_non_negative : forall b: bag 'a, x: 'a. nb_occ x b >= 0
(* equality of bags *)
predicate eq_bag (a b : bag 'a) =
forall x:'a. nb_occ x a = nb_occ x b
axiom bag_extensionality: forall a b : bag 'a. eq_bag a b -> a = b
(* basic constructors of bags *)
function empty_bag : bag 'a
axiom occ_empty : forall x: 'a. nb_occ x empty_bag = 0
lemma is_empty : forall b: bag 'a.
(forall x: 'a. nb_occ x b = 0) -> b = empty_bag
function singleton (x: 'a) : bag 'a = A.set empty_bag x 1
lemma occ_singleton_eq : forall x y: 'a. x = y -> (nb_occ y (singleton x)) = 1
lemma occ_singleton_neq : forall x y: 'a. x <> y -> (nb_occ y (singleton x)) = 0
function union (bag 'a) (bag 'a) : bag 'a
axiom occ_union : forall x: 'a, a b : bag 'a. nb_occ x (union a b) = (nb_occ x a) + (nb_occ x b)
(* union commutative, associative with identity empty_bag *)
lemma Union_comm : forall a b:bag 'a. (union a b) = (union b a)
lemma Union_identity : forall a:bag 'a. (union a empty_bag) = a
lemma Union_assoc : forall a b c:bag 'a.
(union a (union b c)) = (union (union a b) c)
lemma bag_simpl : forall a b c: bag 'a.
(union a b) = (union c b) -> a = c
(* add operation *)
function add (x : 'a) (b: bag 'a) : bag 'a = union (singleton x) b
lemma occ_add_eq : forall b: bag 'a, x y: 'a.
x = y -> nb_occ x (add x b) = (nb_occ x b) + 1
lemma occ_add_neq : forall b: bag 'a, x y: 'a.
x <> y -> nb_occ y (add x b) = (nb_occ y b)
(* cardinality of bags *)
function card (bag 'a) : int
axiom Card_empty : card (empty_bag: bag 'a) = 0
axiom Card_singleton : forall x:'a. card (singleton x) = 1
axiom Card_union: forall x y: bag 'a. card (union x y) = (card x) + (card y)
axiom Card_zero_empty : forall x: bag 'a. card (x) = 0 -> x = empty_bag
end
(*
Local Variables:
compile-command: "why3ide -I . proofs"
End:
*)
theory Bag_integers
(* minimum element of a bag of integers *)
use import int.Int
clone import comparison.MinMax with type t = int, predicate ge = Int.(>=)
use export bag.Bag
function min_bag (bag int) : int
axiom Min_bag_singleton : forall x:int. min_bag (singleton x) = x
axiom Min_bag_union : forall x y:bag int.
min_bag (union x y) = min (min_bag x) (min_bag y)
lemma Min_bag_union1 : forall x y: bag int, a: int.
x = (add a y) -> min_bag x = min a (min_bag y)
lemma Min_bag_union2 : forall x : bag int, a: int.
a <= min_bag x -> a <= min_bag (add a x)
end
(*
Local Variables:
compile-command: "why3ide -I . proofs"
End:
*)
theory Elements
use import int.Int
use import bag.Bag
use map.Map as A
type array 'a = A.map int 'a
(* [elements a i j] is the bag of elements in a[i..j[ *)
function elements (a:array 'a) (i j:int) : bag 'a
axiom Elements_empty : forall a:array int, i j:int.
i >= j -> (elements a i j) = empty_bag
axiom Elements_singleton : forall a:array int, i j:int.
j = i + 1 ->
(elements a i j) = (singleton (A.get a i))
axiom Elements_union : forall a:array int, i j k:int.
i <= j <= k ->
(elements a i k) = (union (elements a i j) (elements a j k))
lemma Elements_union1 : forall a:array int, i j :int.
i < j ->
(elements a i j) = (add (A.get a i) (elements a (i+1) j))
lemma Elements_union2 : forall a:array int, i j :int.
i < j ->
(elements a i j) = (add (A.get a (j-1)) (elements a i (j-1)))
lemma Elements_set : forall a:array int, i j:int.
i <= j -> forall k : int. (k < i || k >= j) ->
forall e:int. (elements (A.set a k e) i j) = (elements a i j)
lemma Elements_union3 : forall a:array int, i j k:int.
i <= j ->
(add k (elements a i j)) = (elements (A.set a j k) i (j+1))
lemma Elements_set2 : forall a:array int, i j k:int.
i <= k < j ->
forall e:int. (add (A.get a k) (elements (A.set a k e) i j)) =
(add e (elements a i j))
end
(*
Local Variables:
compile-command: "why3ide -I . proofs"
End:
*)
module HeapSort
(**** logic declarations *****)
use import int.Int
use import elements.Elements
use import bag.Bag
use import bag_of_integers.Bag_integers
use import module ref.Ref
use import module array.Array
use import module array.ArraySorted
use import module abstract_heap.AbstractHeap
lemma Min_of_sorted:
forall a:M.map int int, i n :int.
0 <= i < n -> (M.sorted_sub a 0 n) ->
min_bag (elements a i n) = M.get a i
(* heap sort *)
let heapSort (a : array int) =
{ length a >= 0 }
'Init:
let len = length a in
let h = create len in
for i = 0 to len-1 do
invariant
{ 0 <= i <= len /\
card (model !h) = i /\
model !h = elements a.elts 0 i }
insert h a[i]
done;
for i = 0 to len-1 do
invariant
{ 0 <= i <= len /\
card (model !h) = len - i /\
elements (at a.elts 'Init) 0 len =
union (model !h) (elements a.elts 0 i) /\
sorted_sub a 0 i /\
forall j:int. 0 <= j < i -> a[j] <= min_bag (model !h)
}
a[i] <- extractMin h;
assert { a[i] <= min_bag (model !h) }
done
{ sorted a /\
elements a.elts 0 (length a) =
elements (old a.elts) 0 (length a) }
end
(*
Local Variables:
compile-command: "why3ide -I . proofs"
End:
*)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Theorem Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a b c.
apply bag_extensionality; intro x.
do 4 rewrite occ_union; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Theorem Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a b.
apply bag_extensionality; intro x.
do 2 rewrite occ_union; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Theorem Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a.
apply bag_extensionality; intro x.
rewrite occ_union.
rewrite occ_empty; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall (a:Type), (map a Z).
Set Contextual Implicit.
Implicit Arguments empty_bag.
Unset Contextual Implicit.
Axiom occ_empty : forall (a:Type), forall (x:a), ((get (empty_bag:(map a Z))
x) = 0%Z).
Axiom is_empty : forall (a:Type), forall (b:(map a Z)), (forall (x:a),
((get b x) = 0%Z)) -> (b = (empty_bag:(map a Z))).
Axiom occ_singleton_eq : forall (a:Type), forall (x:a) (y:a), (x = y) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 1%Z).
Axiom occ_singleton_neq : forall (a:Type), forall (x:a) (y:a), (~ (x = y)) ->
((get (set (empty_bag:(map a Z)) x 1%Z) y) = 0%Z).
Parameter union: forall (a:Type), (map a Z) -> (map a Z) -> (map a Z).
Implicit Arguments union.
Axiom occ_union : forall (a:Type), forall (x:a) (a1:(map a Z)) (b:(map a Z)),
((get (union a1 b) x) = ((get a1 x) + (get b x))%Z).
Axiom Union_comm : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z)),
((union a1 b) = (union b a1)).
Axiom Union_identity : forall (a:Type), forall (a1:(map a Z)), ((union a1
(empty_bag:(map a Z))) = a1).
Axiom Union_assoc : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 (union b c)) = (union (union a1 b) c)).
Theorem bag_simpl : forall (a:Type), forall (a1:(map a Z)) (b:(map a Z))
(c:(map a Z)), ((union a1 b) = (union c b)) -> (a1 = c).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X a b c H_union.
apply bag_extensionality; intro x.
assert (h: (get (union a b) x) = (get (union c b) x))
by (rewrite H_union; auto).
do 2 rewrite occ_union in h; auto with zarith.
Qed.
(* DO NOT EDIT BELOW *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Definition bag (a:Type) := (map a Z).
Axiom occ_non_negative : forall (a:Type), forall (b:(map a Z)) (x:a),
(0%Z <= (get b x))%Z.
Definition eq_bag (a:Type)(a1:(map a Z)) (b:(map a Z)): Prop := forall (x:a),
((get a1 x) = (get b x)).
Implicit Arguments eq_bag.
Axiom bag_extensionality : forall (a:Type), forall (a1:(map a Z)) (b:(map a
Z)), (eq_bag a1 b) -> (a1 = b).