 ### add a new version of vacid_0_sparse_array_2 using type invariants

parent eec946f3
 module SparseArray (* If the sparse array contains three elements x y z, at index a b c respectively, then the three arrays look like this: b a c values +-----+-+---+-+----+-+----+ | |y| |x| |z| | +-----+-+---+-+----+-+----+ index +-----+-+---+-+----+-+----+ | |1| |0| |2| | +-----+-+---+-+----+-+----+ 0 1 2 n=3 back +-+-+-+-------------------+ |a|b|c| | +-+-+-+-------------------+ *) use import int.Int use import module array.Array as A constant maxlen : int = 1000 type sparse_array 'a = {| values : array 'a; index : array int; back : array int; mutable card : int; def : 'a; |} invariant { 0 <= card <= A.length values <= maxlen /\ A.length values = A.length index = A.length back /\ forall i : int. 0 <= i < card -> 0 <= back[i] < A.length values /\ index[back[i]] = i } predicate is_elt (a: sparse_array 'a) (i: int) = 0 <= a.index[i] < a.card /\ a.back[a.index[i]] = i function value (a: sparse_array 'a) (i: int) : 'a = if is_elt a i then a.values[i] else a.def function length (a: sparse_array 'a) : int = A.length a.values (* creation *) val malloc : n:int -> {} array 'a { A.length result = n } let create (sz: int) (d: 'a) = { 0 <= sz <= maxlen } {| values = malloc sz; index = malloc sz; back = malloc sz; card = 0; def = d |} { result.card = 0 /\ result.def = d /\ length result = sz } (* access *) let test (a: sparse_array 'a) i = { 0 <= i < length a } 0 <= a.index[i] && a.index[i] < a.card && a.back[a.index[i]] = i { result=True <-> is_elt a i } let get (a: sparse_array 'a) i = { 0 <= i < length a } if test a i then a.values[i] else a.def { result = value a i } (* assignment *) use map.MapInjection as MI lemma permutation : forall a: sparse_array 'a. (* sparse_array invariant *) (0 <= a.card <= A.length a.values <= maxlen /\ A.length a.values = A.length a.index = A.length a.back /\ forall i : int. 0 <= i < a.card -> 0 <= a.back[i] < A.length a.values /\ a.index[a.back[i]] = i) -> (* sparse_array invariant *) a.card = a.length -> forall i: int. 0 <= i < a.length -> is_elt a i let set (a: sparse_array 'a) i v = { 0 <= i < length a } a.values[i] <- v; if not (test a i) then begin assert { a.card < length a }; a.index[i] <- a.card; a.back[a.card] <- i; a.card <- a.card + 1 end { value a i = v /\ forall j:int. j <> i -> value a j = value (old a) j } end module Harness use import module SparseArray type elt constant default : elt constant c1 : elt constant c2 : elt let harness () = let a = create 10 default in let b = create 20 default in let get_a_5 = get a 5 in assert { get_a_5 = default }; let get_b_7 = get b 7 in assert { get_b_7 = default }; set a 5 c1; set b 7 c2; let get_a_5 = get a 5 in assert { get_a_5 = c1 }; let get_b_7 = get b 7 in assert { get_b_7 = c2 }; let get_a_7 = get a 7 in assert { get_a_7 = default }; let get_b_5 = get b 5 in assert { get_b_5 = default }; let get_a_0 = get a 0 in assert { get_a_0 = default }; let get_b_0 = get b 0 in assert { get_b_0 = default }; () end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/vacid_0_sparse_array.gui" End: *)
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. (* Why3 assumption *) Definition unit := unit. 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 (a:Type) (b:Type), b -> (map a b). Set Contextual Implicit. Implicit Arguments const. Unset Contextual Implicit. Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). (* Why3 assumption *) Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. (* Why3 assumption *) Definition elts (a:Type)(v:(array a)): (map Z a) := match v with | (mk_array x x1) => x1 end. Implicit Arguments elts. (* Why3 assumption *) Definition length (a:Type)(v:(array a)): Z := match v with | (mk_array x x1) => x end. Implicit Arguments length. (* Why3 assumption *) Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). Implicit Arguments get1. (* Why3 assumption *) Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)). Implicit Arguments set1. (* Why3 assumption *) Inductive sparse_array (a:Type) := | mk_sparse_array : (array a) -> (array Z) -> (array Z) -> Z -> a -> sparse_array a. Implicit Arguments mk_sparse_array. (* Why3 assumption *) Definition def (a:Type)(v:(sparse_array a)): a := match v with | (mk_sparse_array x x1 x2 x3 x4) => x4 end. Implicit Arguments def. (* Why3 assumption *) Definition card (a:Type)(v:(sparse_array a)): Z := match v with | (mk_sparse_array x x1 x2 x3 x4) => x3 end. Implicit Arguments card. (* Why3 assumption *) Definition back (a:Type)(v:(sparse_array a)): (array Z) := match v with | (mk_sparse_array x x1 x2 x3 x4) => x2 end. Implicit Arguments back. (* Why3 assumption *) Definition index (a:Type)(v:(sparse_array a)): (array Z) := match v with | (mk_sparse_array x x1 x2 x3 x4) => x1 end. Implicit Arguments index. (* Why3 assumption *) Definition values (a:Type)(v:(sparse_array a)): (array a) := match v with | (mk_sparse_array x x1 x2 x3 x4) => x end. Implicit Arguments values. (* Why3 assumption *) Definition is_elt (a:Type)(a1:(sparse_array a)) (i:Z): Prop := ((0%Z <= (get1 (index a1) i))%Z /\ ((get1 (index a1) i) < (card a1))%Z) /\ ((get1 (back a1) (get1 (index a1) i)) = i). Implicit Arguments is_elt. Parameter value: forall (a:Type), (sparse_array a) -> Z -> a. Implicit Arguments value. Axiom value_def : forall (a:Type), forall (a1:(sparse_array a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (get1 (values a1) i))) /\ ((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))). (* Why3 assumption *) Definition length1 (a:Type)(a1:(sparse_array a)): Z := (length (values a1)). Implicit Arguments length1. (* Why3 assumption *) Definition injective(a:(map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) -> ((~ (i = j)) -> ~ ((get a i) = (get a j)))). (* Why3 assumption *) Definition surjective(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\ ((get a j) = i). (* Why3 assumption *) Definition range(a:(map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (get a i))%Z /\ ((get a i) < n)%Z). Axiom injective_surjective : forall (a:(map Z Z)) (n:Z), (injective a n) -> ((range a n) -> (surjective a n)). Require Import Why3. Ltac ae := why3 "alt-ergo". (* Why3 goal *) Theorem permutation : forall (a:Type), forall (a1:(sparse_array a)), ((((0%Z <= (card a1))%Z /\ ((card a1) <= (length (values a1)))%Z) /\ ((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 <= (get1 (back a1) i))%Z /\ ((get1 (back a1) i) < (length (values a1)))%Z) /\ ((get1 (index a1) (get1 (back a1) i)) = i)))) -> (((card a1) = (length1 a1)) -> forall (i:Z), ((0%Z <= i)%Z /\ (i < (length1 a1))%Z) -> (is_elt a1 i)). intros a a1. destruct a1 as ((n0, a_values), (n1, a_index), (n2, a_back), a_card, a_def); simpl. unfold is_elt, length1, get1; simpl. intro H; decompose [and] H; clear H. clear a_values a_def H0 H3 H4. subst n1 n2. intros. subst a_card. assert (inj: injective a_back n0) by ae. assert (rng: range a_back n0) by ae. generalize (injective_surjective a_back n0 inj rng); intro surj. destruct (surj i H0) as (j, (hj1, hj2)). ae. Qed.
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