Commit 0ba5e6d0 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

VACID-0: red black trees almost complete

parent 20dcfdcd
......@@ -162,7 +162,6 @@ why3.conf
/examples/programs/course/
/examples/programs/wcet_hull/
/examples/programs/binary_search2/
/examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
/examples/programs/algo63/
......
module M
use import module ref.Ref
module RedBlackTree
(* Red-black trees (data type) *)
......@@ -35,6 +34,54 @@ module M
predicate gt_tree (x : key) (t : tree) =
forall k : key. forall v : value. memt t k v -> x < k
lemma lt_leaf: forall x: key. lt_tree x Leaf
lemma gt_leaf: forall x: key. gt_tree x Leaf
lemma lt_tree_node:
forall x y: key, v: value, l r: tree, c: color.
lt_tree x l -> lt_tree x r -> y < x -> lt_tree x (Node c l y v r)
lemma gt_tree_node:
forall x y: key, v: value, l r: tree, c: color.
gt_tree x l -> gt_tree x r -> x < y -> gt_tree x (Node c l y v r)
lemma lt_node_lt:
forall x y: key, v: value, l r: tree, c: color.
lt_tree x (Node c l y v r) -> y < x
lemma gt_node_gt:
forall x y: key, v: value, l r: tree, c: color.
gt_tree x (Node c l y v r) -> x < y
lemma lt_left:
forall x y: key, v: value, l r: tree, c : color.
lt_tree x (Node c l y v r) -> lt_tree x l
lemma lt_right:
forall x y: key, v: value, l r: tree, c: color.
lt_tree x (Node c l y v r) -> lt_tree x r
lemma gt_left:
forall x y: key, v: value, l r: tree, c: color.
gt_tree x (Node c l y v r) -> gt_tree x l
lemma gt_right:
forall x y: key, v: value, l r: tree, c: color.
gt_tree x (Node c l y v r) -> gt_tree x r
lemma lt_tree_not_in:
forall x: key, t: tree. lt_tree x t -> forall v: value. not (memt t x v)
lemma lt_tree_trans:
forall x y: key. x < y -> forall t: tree. lt_tree x t -> lt_tree y t
lemma gt_tree_not_in :
forall x: key, t: tree. gt_tree x t -> forall v: value. not (memt t x v)
lemma gt_tree_trans :
forall x y: key. y < x -> forall t: tree. gt_tree x t -> gt_tree y t
predicate bst (t : tree) =
match t with
| Leaf -> true
......@@ -43,6 +90,26 @@ module M
lemma bst_Leaf : bst Leaf
lemma bst_left:
forall k: key, v: value, l r: tree, c: color. bst (Node c l k v r) -> bst l
lemma bst_right:
forall k: key, v: value, l r: tree, c: color. bst (Node c l k v r) -> bst r
lemma bst_color:
forall c c': color, k: key, v: value, l r: tree.
bst (Node c l k v r) -> bst (Node c' l k v r)
lemma rotate_left:
forall kx ky: key, vx vy: value, a b c: tree, c1 c2 c3 c4: color.
bst (Node c1 a kx vx (Node c2 b ky vy c)) ->
bst (Node c3 (Node c4 a kx vx b) ky vy c)
lemma rotate_right:
forall kx ky: key, vx vy: value, a b c: tree, c1 c2 c3 c4: color.
bst (Node c3 (Node c4 a kx vx b) ky vy c) ->
bst (Node c1 a kx vx (Node c2 b ky vy c))
(* [rbtree n t]: red black tree invariant
[t] is a properly balanced red-black tree, i.e. it
satisfies the following two invariants:
......@@ -66,11 +133,20 @@ module M
rbtree (n-1) l /\ rbtree (n-1) r
end
lemma rbtree_Leaf : rbtree 0 Leaf
lemma rbtree_Leaf:
rbtree 0 Leaf
lemma rbtree_Node1 :
lemma rbtree_Node1:
forall k:key, v:value. rbtree 0 (Node Red Leaf k v Leaf)
lemma rbtree_left:
forall x: key, v: value, l r: tree, c: color.
(exists n: int. rbtree n (Node c l x v r)) -> exists n: int. rbtree n l
lemma rbtree_right:
forall x: key, v: value, l r: tree, c: color.
(exists n: int. rbtree n (Node c l x v r)) -> exists n: int. rbtree n r
(* lookup *)
exception Not_found
......@@ -101,6 +177,17 @@ module M
rbtree (n-1) l /\ rbtree (n-1) r
end
lemma rbtree_almost_rbtree:
forall n: int, t: tree. rbtree n t -> almost_rbtree n t
lemma rbtree_almost_rbtree_ex:
forall s: tree.
(exists n: int. rbtree n s) -> exists n: int. almost_rbtree n s
lemma almost_rbtree_rbtree_black:
forall x: key, v: value, l r: tree, n: int.
almost_rbtree n (Node Black l x v r) -> rbtree n (Node Black l x v r)
(** [lbalance c x l r] acts as a black node constructor,
solving a possible red-red conflict on [l], using the following
schema:
......@@ -157,7 +244,7 @@ module M
conflict when [s] is red. *)
let rec insert (t : tree) (k : key) (v : value) : tree =
{ bst t }
{ bst t /\ exists n: int. rbtree n t }
match t with
| Leaf ->
Node Red Leaf k v Leaf
......@@ -190,8 +277,15 @@ module M
forall k':key, v':value.
memt result k' v' <-> if k' = k then v' = v else memt t k' v' }
end
module Vacid0
(* the VACID-0 interface = mutable map with default value*)
use import module ref.Ref
use import module RedBlackTree
type rbt = (value, tree)
predicate inv (r : rbt) =
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Definition key := Z.
Definition value := Z.
Inductive color :=
| Red : color
| Black : color .
Inductive tree :=
| Leaf : tree
| Node : color -> tree -> Z -> Z -> tree -> tree .
Set Implicit Arguments.
Fixpoint memt(t:tree) (k:Z) (v:Z) {struct t}: Prop :=
match t with
| Leaf => False
| (Node _ l kqt vqt r) => ((k = kqt) /\ (v = vqt)) \/ ((memt l k v) \/
(memt r k v))
end.
Unset Implicit Arguments.
Axiom memt_color : forall (l:tree) (r:tree) (k:Z) (kqt:Z) (v:Z) (vqt:Z)
(c:color) (cqt:color), (memt (Node c l k v r) kqt vqt) -> (memt (Node cqt l
k v r) kqt vqt).
Definition lt_tree(x:Z) (t:tree): Prop := forall (k:Z), forall (v:Z), (memt t
k v) -> (k < x)%Z.
Definition gt_tree(x:Z) (t:tree): Prop := forall (k:Z), forall (v:Z), (memt t
k v) -> (x < k)%Z.
Set Implicit Arguments.
Fixpoint bst(t:tree) {struct t}: Prop :=
match t with
| Leaf => True
| (Node _ l k v r) => (bst l) /\ ((bst r) /\ ((lt_tree k l) /\ (gt_tree k
r)))
end.
Unset Implicit Arguments.
Axiom bst_Leaf : (bst Leaf).
Definition is_not_red(t:tree): Prop :=
match t with
| (Node Red _ _ _ _) => False
| (Leaf|(Node Black _ _ _ _)) => True
end.
Set Implicit Arguments.
Fixpoint rbtree(n:Z) (t:tree) {struct t}: Prop :=
match t with
| Leaf => (n = 0%Z)
| (Node Red l _ _ r) => (rbtree n l) /\ ((rbtree n r) /\ ((is_not_red l) /\
(is_not_red r)))
| (Node Black l _ _ r) => (rbtree (n - 1%Z)%Z l) /\ (rbtree (n - 1%Z)%Z r)
end.
Unset Implicit Arguments.
Axiom rbtree_Leaf : (rbtree 0%Z Leaf).
Axiom rbtree_Node1 : forall (k:Z) (v:Z), (rbtree 0%Z (Node Red Leaf k v
Leaf)).
Definition almost_rbtree(n:Z) (t:tree): Prop :=
match t 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.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_add : forall (t:tree), forall (k:Z), forall (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 (kqt:Z)
(vqt:Z), ((memt result kqt vqt) \/ (((kqt = k) -> (vqt = v)) /\
((~ (kqt = k)) -> (memt t kqt vqt)))) -> ((memt result kqt vqt) /\
(((kqt = k) /\ (vqt = v)) \/ ((~ (kqt = k)) /\ (memt t kqt vqt))))))) ->
match result with
| (Node _ l kqt vqt r) => exists n:Z, (rbtree n (Node Black l kqt vqt r))
| Leaf => True
end).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
destruct result; auto.
destruct H2 as (n, h). clear H3.
generalize (H0 n h); clear H0.
intros.
destruct c; intuition.
(* c = Red *)
exists (n+1)%Z; intuition.
simpl rbtree. replace (n+1-1)%Z with n by omega.
intuition.
(* c = Black *)
exists n; intuition.
simpl rbtree.
intuition.
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.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Definition key := Z.
Definition value := Z.
Inductive color :=
| Red : color
| Black : color .
Inductive tree :=
| Leaf : tree
| Node : color -> tree -> Z -> Z -> tree -> tree .
Set Implicit Arguments.
Fixpoint memt(t:tree) (k:Z) (v:Z) {struct t}: Prop :=
match t with
| Leaf => False
| (Node _ l kqt vqt r) => ((k = kqt) /\ (v = vqt)) \/ ((memt l k v) \/
(memt r k v))
end.
Unset Implicit Arguments.
Axiom memt_color : forall (l:tree) (r:tree) (k:Z) (kqt:Z) (v:Z) (vqt:Z)
(c:color) (cqt:color), (memt (Node c l k v r) kqt vqt) -> (memt (Node cqt l
k v r) kqt vqt).
Definition lt_tree(x:Z) (t:tree): Prop := forall (k:Z), forall (v:Z), (memt t
k v) -> (k < x)%Z.
Definition gt_tree(x:Z) (t:tree): Prop := forall (k:Z), forall (v:Z), (memt t
k v) -> (x < k)%Z.
Axiom lt_leaf : forall (x:Z), (lt_tree x Leaf).
Axiom gt_leaf : forall (x:Z), (gt_tree x Leaf).
Axiom lt_tree_node : forall (x:Z) (y:Z) (v:Z) (l:tree) (r:tree) (c:color),
(lt_tree x l) -> ((lt_tree x r) -> ((y < x)%Z -> (lt_tree x (Node c l y v
r)))).
Axiom gt_tree_node : forall (x:Z) (y:Z) (v:Z) (l:tree) (r:tree) (c:color),
(gt_tree x l) -> ((gt_tree x r) -> ((x < y)%Z -> (gt_tree x (Node c l y v
r)))).
Axiom lt_node_lt : forall (x:Z) (y:Z) (v:Z) (l:tree) (r:tree) (c:color),
(lt_tree x (Node c l y v r)) -> (y < x)%Z.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem gt_node_gt : forall (x:Z) (y:Z) (v:Z) (l:tree) (r:tree) (c:color),
(gt_tree x (Node c l y v r)) -> (x < y)%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
red in H.
generalize (H y v); intuition.
apply H0.
red; intuition.
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.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
Definition key := Z.
Definition value := Z.
Inductive color :=
| Red : color
| Black : color .
Inductive tree :=
| Leaf : tree
| Node : color -> tree -> Z -> Z -> tree -> tree .
Set Implicit Arguments.
Fixpoint memt(t:tree) (k:Z) (v:Z) {struct t}: Prop :=
match t with
| Leaf => False
| (Node _ l kqt vqt r) => ((k = kqt) /\ (v = vqt)) \/ ((memt l k v) \/
(memt r k v))
end.
Unset Implicit Arguments.
Axiom memt_color : forall (l:tree) (r:tree) (k:Z) (kqt:Z) (v:Z) (vqt:Z)
(c:color) (cqt:color), (memt (Node c l k v r) kqt vqt) -> (memt (Node cqt l
k v r) kqt vqt).
Definition lt_tree(x:Z) (t:tree): Prop := forall (k:Z), forall (v:Z), (memt t
k v) -> (k < x)%Z.
Definition gt_tree(x:Z) (t:tree): Prop := forall (k:Z), forall (v:Z), (memt t
k v) -> (x < k)%Z.
Axiom lt_leaf : forall (x:Z), (lt_tree x Leaf).
Axiom gt_leaf : forall (x:Z), (gt_tree x Leaf).
Axiom lt_tree_node : forall (x:Z) (y:Z) (v:Z) (l:tree) (r:tree) (c:color),
(lt_tree x l) -> ((lt_tree x r) -> ((y < x)%Z -> (lt_tree x (Node c l y v
r)))).
Axiom gt_tree_node : forall (x:Z) (y:Z) (v:Z) (l:tree) (r:tree) (c:color),
(gt_tree x l) -> ((gt_tree x r) -> ((x < y)%Z -> (gt_tree x (Node c l y v
r)))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem lt_node_lt : forall (x:Z) (y:Z) (v:Z) (l:tree) (r:tree) (c:color),
(lt_tree x (Node c l y v r)) -> (y < x)%Z.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
red in H.
generalize (H y v).
intuition.
apply H0.
red; intuition.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
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