Commit 2a84e635 authored by Martin Clochard's avatar Martin Clochard

Merge branch 'new_system' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into new_system

parents 553a36bc ce7bf93b
bag.mlw
bellman_ford.mlw
bignum.mlw
bitwalker.mlw
counting_sort.mlw
cursor.mlw
dijkstra.mlw
......@@ -28,9 +27,6 @@ sum_of_digits.mlw
topological_sorting.mlw
tortoise_and_hare.mlw
tree_height.mlw
unraveling_a_card_trick.mlw
vacid_0_build_maze.mlw
vacid_0_red_black_trees.mlw
vacid_0_sparse_array.mlw
verifythis_fm2012_LRS.mlw
verifythis_fm2012_treedel.mlw
......
This diff is collapsed.
This diff is collapsed.
......@@ -7,10 +7,6 @@ Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Definition key := Z.
......@@ -166,40 +162,31 @@ Axiom almost_rbtree_rbtree_black : forall (x:Z) (v:Z) (l:tree) (r:tree)
(n:Z), (almost_rbtree n (Node Black l x v r)) -> (rbtree n (Node Black l x
v r)).
(* Why3 goal *)
Theorem WP_parameter_add : forall (t:tree) (k:Z) (v:Z), ((bst t) /\
exists n:Z, (rbtree n t)) -> (((bst t) /\ exists n:Z, (rbtree n t)) ->
forall (result:tree), ((bst result) /\ ((forall (n:Z), (rbtree n t) ->
(match result with
| Leaf => (n = 0%Z)
| (Node Red l _ _ r) => (rbtree n l) /\ (rbtree n r)
| (Node Black l _ _ r) => (rbtree (n - 1%Z)%Z l) /\ (rbtree (n - 1%Z)%Z r)
end /\
(match t with
| (Node Red _ _ _ _) => False
| (Leaf|(Node Black _ _ _ _)) => True
end -> (rbtree n result)))) /\ ((memt result k v) /\ forall (k':Z) (v':Z),
((memt result k' v') \/ (((k' = k) -> (v' = v)) /\ ((~ (k' = k)) -> (memt t
k' v')))) -> ((memt result k' v') /\ (((k' = k) /\ (v' = v)) \/
((~ (k' = k)) /\ (memt t k' v'))))))) -> forall (x:color) (x1:tree) (x2:Z)
(x3:Z) (x4:tree), (result = (Node x x1 x2 x3 x4)) -> exists n:Z, (rbtree n
(Node Black x1 x2 x3 x4))).
intros t k v (h1,(n,h2)) _ result (h5,(h6,(h7,h8))) c x1 x2
x3 x4 h9.
Theorem VC_add : forall (t:tree) (k:Z) (v:Z), ((bst t) /\ exists n:Z, (rbtree
n t)) -> forall (o:tree), ((bst o) /\ ((forall (n:Z), (rbtree n t) ->
((almost_rbtree n o) /\ ((is_not_red t) -> (rbtree n o)))) /\ ((memt o k
v) /\ forall (k':Z) (v':Z), ((memt o k' v') \/ (((k' = k) -> (v' = v)) /\
((~ (k' = k)) -> (memt t k' v')))) -> ((memt o k' v') /\ (((k' = k) /\
(v' = v)) \/ ((~ (k' = k)) /\ (memt t k' v'))))))) -> forall (result:tree),
(exists x:color, (exists x1:tree, (exists x2:Z, (exists x3:Z,
(exists x4:tree, (o = (Node x x1 x2 x3 x4)) /\ (result = (Node Black x1 x2
x3 x4))))))) -> exists n:Z, (rbtree n result).
intros t k v (h1,(n,h2)) o (h3,(h4,(h5,h6))) result
(x,(x1,(x2,(x3,(x4,(h7,h8)))))).
subst.
intuition.
generalize (h6 n h2); clear h6.
generalize (h4 n h2); clear h4.
intros.
destruct c; intuition.
destruct x; intuition.
(* c = Red *)
exists (n+1)%Z; intuition.
simpl rbtree. replace (n+1-1)%Z with n by omega.
intuition.
simpl in H0. intuition.
(* c = Black *)
exists n; intuition.
simpl rbtree.
intuition.
Qed.
......@@ -2,6 +2,7 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require map.Map.
Require map.Occ.
......@@ -10,84 +11,70 @@ Require map.MapInjection.
(* Why3 assumption *)
Definition unit := unit.
(* Why3 assumption *)
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Axiom array : forall (a:Type), Type.
Parameter array_WhyType : forall (a:Type) {a_WT:WhyType a},
WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a).
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array
a)), (0%Z <= (length self))%Z.
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
((elts a1) i).
(* Why3 assumption *)
Inductive sparse_array
(a:Type) :=
| mk_sparse_array : (array a) -> (array Z) -> (array Z) -> Z -> a ->
sparse_array a.
Axiom sparse_array_WhyType : forall (a:Type) {a_WT:WhyType a},
Parameter mixfix_lblsmnrb: forall {a:Type} {a_WT:WhyType a}, (array a) ->
Z -> a -> (array a).
Axiom mixfix_lblsmnrb_spec : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (i:Z) (v:a), ((length (mixfix_lblsmnrb a1 i
v)) = (length a1)) /\ ((elts (mixfix_lblsmnrb a1 i
v)) = (map.Map.set (elts a1) i v)).
Axiom sparse_array : forall (a:Type), Type.
Parameter sparse_array_WhyType : forall (a:Type) {a_WT:WhyType a},
WhyType (sparse_array a).
Existing Instance sparse_array_WhyType.
Implicit Arguments mk_sparse_array [[a]].
(* Why3 assumption *)
Definition def {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): a :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x4
end.
Parameter values: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) ->
(array a).
(* Why3 assumption *)
Definition card {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): Z :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x3
end.
Parameter index: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array
Z).
(* Why3 assumption *)
Definition back {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array Z) :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x2
end.
Parameter back: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array
Z).
(* Why3 assumption *)
Definition index {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array Z) :=
match v with
| (mk_sparse_array x x1 x2 x3 x4) => x1
end.
Parameter card: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z.
(* Why3 assumption *)
Definition values {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array
a) := match v with
| (mk_sparse_array x x1 x2 x3 x4) => x
end.
Parameter def: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> a.
Axiom sparse_array'invariant : forall {a:Type} {a_WT:WhyType a},
forall (self:(sparse_array a)), ((0%Z <= (card self))%Z /\
(((card self) <= (length (values self)))%Z /\
((length (values self)) <= 1000%Z)%Z)) /\
((((length (values self)) = (length (index self))) /\
((length (index self)) = (length (back self)))) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < (card self))%Z) -> (((0%Z <= (mixfix_lbrb (back self)
i))%Z /\ ((mixfix_lbrb (back self) i) < (length (values self)))%Z) /\
((mixfix_lbrb (index self) (mixfix_lbrb (back self) i)) = i))).
(* Why3 assumption *)
Definition is_elt {a:Type} {a_WT:WhyType a} (a1:(sparse_array a))
(i:Z): Prop := ((0%Z <= (get (index a1) i))%Z /\ ((get (index a1)
i) < (card a1))%Z) /\ ((get (back a1) (get (index a1) i)) = i).
(i:Z): Prop := ((0%Z <= (mixfix_lbrb (index a1) i))%Z /\
((mixfix_lbrb (index a1) i) < (card a1))%Z) /\ ((mixfix_lbrb (back a1)
(mixfix_lbrb (index a1) i)) = i).
Parameter value: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z ->
a.
Axiom value_def : forall {a:Type} {a_WT:WhyType a}, forall (a1:(sparse_array
a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (get (values a1) i))) /\
((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))).
a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (mixfix_lbrb (values a1)
i))) /\ ((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))).
(* Why3 assumption *)
Definition length1 {a:Type} {a_WT:WhyType a} (a1:(sparse_array a)): Z :=
......@@ -103,10 +90,11 @@ Theorem permutation : forall {a:Type} {a_WT:WhyType a},
((length (values a1)) <= 1000%Z)%Z)) /\
((((length (values a1)) = (length (index a1))) /\
((length (index a1)) = (length (back a1)))) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < (card a1))%Z) -> (((0%Z <= (get (back a1) i))%Z /\
((get (back a1) i) < (length (values a1)))%Z) /\ ((get (index a1)
(get (back a1) i)) = i)))) -> (((card a1) = (length1 a1)) -> forall (i:Z),
((0%Z <= i)%Z /\ (i < (length1 a1))%Z) -> (is_elt a1 i)).
((0%Z <= i)%Z /\ (i < (card a1))%Z) -> (((0%Z <= (mixfix_lbrb (back a1)
i))%Z /\ ((mixfix_lbrb (back a1) i) < (length (values a1)))%Z) /\
((mixfix_lbrb (index a1) (mixfix_lbrb (back a1) i)) = i)))) ->
(((card a1) = (length1 a1)) -> forall (i:Z), ((0%Z <= i)%Z /\
(i < (length1 a1))%Z) -> (is_elt a1 i)).
(* Why3 intros a a_WT a1 ((h1,(h2,h3)),((h4,h5),h6)) h7 i (h8,h9). *)
intros a _a a1.
destruct a1 as ((n0, a_values), (n1, a_index), (n2, a_back), a_card, a_def); simpl.
......
This diff is collapsed.
......@@ -1237,6 +1237,13 @@ let load_option attr g =
let load_ident elt =
let name = string_attribute "name" elt in
(* temporary hack to update sessions from WhyML 0.8x *)
let name =
if String.length name >= 13 &&
String.sub name 0 13 = "WP_parameter " then
"VC " ^ String.sub name 13 (String.length name - 13)
else name
in
let label = List.fold_left
(fun acc label ->
match label with
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment