Commit e9fc204a by Jean-Christophe

### new version of vstte12_ring_buffer using a ghost field

parent 1136e75e
 (* The 2nd Verified Software Competition (VSTTE 2012) https://sites.google.com/site/vstte2012/compet Problem 3: Queue data structure implemented using a ring buffer Alternative solution using a model stored in a ghost field *) module RingBuffer use import int.Int use import list.NthLengthAppend as L use import module array.Array type buffer 'a = {| mutable first: int; mutable len : int; data : array 'a; ghost mutable sequence: list 'a; |} (* total capacity of the buffer *) function size (b: buffer 'a) : int = Array.length b.data (* length = number of elements *) function length (b: buffer 'a) : int = b.len predicate buffer_invariant (b: buffer 'a) = 0 <= b.first < size b /\ 0 <= b.len <= size b /\ b.len = L.length b.sequence /\ forall i: int. 0 <= i < b.len -> (b.first + i < size b -> nth i b.sequence = Some b.data[b.first + i]) /\ (0 <= b.first + i - size b -> nth i b.sequence = Some b.data[b.first + i - size b]) (* code *) let create (n: int) (dummy: 'a) = { n > 0 } {| first = 0; len = 0; data = make n dummy; sequence = Nil |} { buffer_invariant result /\ size result = n /\ result.sequence = Nil } let length (b: buffer 'a) = { buffer_invariant b } b.len { result = length b } let clear (b: buffer 'a) = { buffer_invariant b } ghost b.sequence <- Nil; b.len <- 0 { buffer_invariant b /\ length b = 0 /\ b.sequence = Nil } let push (b: buffer 'a) (x: 'a) = { length b < size b /\ buffer_invariant b } ghost b.sequence <- b.sequence ++ Cons x Nil; let i = b.first + b.len in let n = Array.length b.data in b.data[if i >= n then i - n else i] <- x; b.len <- b.len + 1 { buffer_invariant b /\ length b = (old (length b)) + 1 /\ b.sequence = (old b.sequence) ++ Cons x Nil } let head (b: buffer 'a) = { length b > 0 /\ buffer_invariant b } b.data[b.first] { match b.sequence with Nil -> false | Cons x _ -> result = x end } let pop (b: buffer 'a) = { length b > 0 /\ buffer_invariant b } ghost match b.sequence with Nil -> absurd | Cons _ s -> b.sequence <- s end; let r = b.data[b.first] in b.len <- b.len - 1; let n = Array.length b.data in b.first <- b.first + 1; if b.first = n then b.first <- 0; r { buffer_invariant b /\ length b = (old (length b)) - 1 /\ match old b.sequence with | Nil -> false | Cons x l -> result = x /\ b.sequence = l end } end module Harness use import module RingBuffer use import list.List let harness () = let b = create 10 0 in push b 1; push b 2; push b 3; let x = pop b in assert { x = 1 }; let x = pop b in assert { x = 2 }; let x = pop b in assert { x = 3 }; () let harness2 () = let b = create 3 0 in push b 1; assert { sequence b = Cons 1 Nil }; push b 2; assert { sequence b = Cons 1 (Cons 2 Nil) }; push b 3; assert { sequence b = Cons 1 (Cons 2 (Cons 3 Nil)) }; let x = pop b in assert { x = 1 }; assert { sequence b = Cons 2 (Cons 3 Nil) }; push b 4; assert { sequence b = Cons 2 (Cons 3 (Cons 4 Nil)) }; let x = pop b in assert { x = 2 }; assert { sequence b = Cons 3 (Cons 4 Nil) }; let x = pop b in assert { x = 3 }; assert { sequence b = Cons 4 Nil }; let x = pop b in assert { x = 4 }; () use import int.Int let test (x: int) (y: int) (z: int) = let b = create 2 0 in push b x; push b y; assert { sequence b = Cons x (Cons y Nil) }; let h = pop b in assert { h = x }; assert { sequence b = Cons y Nil }; push b z; assert { sequence b = Cons y (Cons z Nil) }; let h = pop b in assert { h = y }; let h = pop b in assert { h = z } end (* Local Variables: compile-command: "why3ide vstte12_ring_buffer_2.mlw" 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. (* Why3 assumption *) Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. (* Why3 assumption *) Inductive option (a:Type) := | None : option a | Some : a -> option a. Set Contextual Implicit. Implicit Arguments None. Unset Contextual Implicit. Implicit Arguments Some. Parameter nth: forall (a:Type), Z -> (list a) -> (option a). Implicit Arguments nth. Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)), match l with | Nil => ((nth n l) = (None :(option a))) | (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) -> ((nth n l) = (nth (n - 1%Z)%Z r))) end. (* Why3 assumption *) Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Axiom nth_none_1 : forall (a:Type), forall (l:(list a)) (i:Z), (i < 0%Z)%Z -> ((nth i l) = (None :(option a))). Axiom nth_none_2 : forall (a:Type), forall (l:(list a)) (i:Z), ((length l) <= i)%Z -> ((nth i l) = (None :(option a))). Axiom nth_none_3 : forall (a:Type), forall (l:(list a)) (i:Z), ((nth i l) = (None :(option a))) -> ((i < 0%Z)%Z \/ ((length l) <= i)%Z). (* Why3 assumption *) Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). (* Why3 assumption *) Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Axiom nth_append_1 : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (i:Z), (i < (length l1))%Z -> ((nth i (infix_plpl l1 l2)) = (nth i l1)). Axiom nth_append_2 : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (i:Z), ((length l1) <= i)%Z -> ((nth i (infix_plpl l1 l2)) = (nth (i - (length l1))%Z l2)). 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 length1 (a:Type)(v:(array a)): Z := match v with | (mk_array x x1) => x end. Implicit Arguments length1. (* 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 (length1 a1) (set (elts a1) i v)). Implicit Arguments set1. (* Why3 assumption *) Inductive buffer (a:Type) := | mk_buffer : Z -> Z -> (array a) -> (list a) -> buffer a. Implicit Arguments mk_buffer. (* Why3 assumption *) Definition sequence (a:Type)(v:(buffer a)): (list a) := match v with | (mk_buffer x x1 x2 x3) => x3 end. Implicit Arguments sequence. (* Why3 assumption *) Definition data (a:Type)(v:(buffer a)): (array a) := match v with | (mk_buffer x x1 x2 x3) => x2 end. Implicit Arguments data. (* Why3 assumption *) Definition len (a:Type)(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2 x3) => x1 end. Implicit Arguments len. (* Why3 assumption *) Definition first (a:Type)(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2 x3) => x end. Implicit Arguments first. (* Why3 assumption *) Definition size (a:Type)(b:(buffer a)): Z := (length1 (data b)). Implicit Arguments size. (* Why3 assumption *) Definition buffer_invariant (a:Type)(b:(buffer a)): Prop := ((0%Z <= (first b))%Z /\ ((first b) < (size b))%Z) /\ (((0%Z <= (len b))%Z /\ ((len b) <= (size b))%Z) /\ (((len b) = (length (sequence b))) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < (len b))%Z) -> (((((first b) + i)%Z < (size b))%Z -> ((nth i (sequence b)) = (Some (get1 (data b) ((first b) + i)%Z)))) /\ ((0%Z <= (((first b) + i)%Z - (size b))%Z)%Z -> ((nth i (sequence b)) = (Some (get1 (data b) (((first b) + i)%Z - (size b))%Z))))))). Implicit Arguments buffer_invariant. Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem WP_parameter_head : forall (a:Type), forall (b:Z) (b1:Z) (b2:(list a)), forall (rho:(map Z a)) (rho1:Z), ((0%Z < b)%Z /\ (buffer_invariant (mk_buffer rho1 b (mk_array b1 rho) b2))) -> (((0%Z <= rho1)%Z /\ (rho1 < b1)%Z) -> match b2 with | Nil => False | (Cons x _) => ((get rho rho1) = x) end). intros a b b1 b2 rho rho1 (h1,h2) (h3,h4). red in h2. destruct b2. simpl in *. omega. intuition. generalize (H5 0%Z). clear H5. ae. Qed.
 (* 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. (* Why3 assumption *) Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. (* Why3 assumption *) Inductive option (a:Type) := | None : option a | Some : a -> option a. Set Contextual Implicit. Implicit Arguments None. Unset Contextual Implicit. Implicit Arguments Some. Parameter nth: forall (a:Type), Z -> (list a) -> (option a). Implicit Arguments nth. Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)), match l with | Nil => ((nth n l) = (None :(option a))) | (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) -> ((nth n l) = (nth (n - 1%Z)%Z r))) end. (* Why3 assumption *) Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Unset Implicit Arguments. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Axiom nth_none_1 : forall (a:Type), forall (l:(list a)) (i:Z), (i < 0%Z)%Z -> ((nth i l) = (None :(option a))). Axiom nth_none_2 : forall (a:Type), forall (l:(list a)) (i:Z), ((length l) <= i)%Z -> ((nth i l) = (None :(option a))). Axiom nth_none_3 : forall (a:Type), forall (l:(list a)) (i:Z), ((nth i l) = (None :(option a))) -> ((i < 0%Z)%Z \/ ((length l) <= i)%Z). (* Why3 assumption *) Set Implicit Arguments. Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Unset Implicit Arguments. Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). (* Why3 assumption *) Set Implicit Arguments. Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Unset Implicit Arguments. Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Axiom nth_append_1 : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (i:Z), (i < (length l1))%Z -> ((nth i (infix_plpl l1 l2)) = (nth i l1)). Axiom nth_append_2 : forall (a:Type), forall (l1:(list a)) (l2:(list a)) (i:Z), ((length l1) <= i)%Z -> ((nth i (infix_plpl l1 l2)) = (nth (i - (length l1))%Z l2)). 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 length1 (a:Type)(v:(array a)): Z := match v with | (mk_array x x1) => x end. Implicit Arguments length1. (* 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 (length1 a1) (set (elts a1) i v)). Implicit Arguments set1. (* Why3 assumption *) Inductive buffer (a:Type) := | mk_buffer : Z -> Z -> (array a) -> (list a) -> buffer a. Implicit Arguments mk_buffer. (* Why3 assumption *) Definition sequence (a:Type)(v:(buffer a)): (list a) := match v with | (mk_buffer x x1 x2 x3) => x3 end. Implicit Arguments sequence. (* Why3 assumption *) Definition data (a:Type)(v:(buffer a)): (array a) := match v with | (mk_buffer x x1 x2 x3) => x2 end. Implicit Arguments data. (* Why3 assumption *) Definition len (a:Type)(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2 x3) => x1 end. Implicit Arguments len. (* Why3 assumption *) Definition first (a:Type)(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2 x3) => x end. Implicit Arguments first. (* Why3 assumption *) Definition size (a:Type)(b:(buffer a)): Z := (length1 (data b)). Implicit Arguments size. (* Why3 assumption *) Definition buffer_invariant (a:Type)(b:(buffer a)): Prop := ((0%Z <= (first b))%Z /\ ((first b) < (size b))%Z) /\ (((0%Z <= (len b))%Z /\ ((len b) <= (size b))%Z) /\ (((len b) = (length (sequence b))) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < (len b))%Z) -> (((((first b) + i)%Z < (size b))%Z -> ((nth i (sequence b)) = (Some (get1 (data b) ((first b) + i)%Z)))) /\ ((0%Z <= (((first b) + i)%Z - (size b))%Z)%Z -> ((nth i (sequence b)) = (Some (get1 (data b) (((first b) + i)%Z - (size b))%Z))))))). Implicit Arguments buffer_invariant. Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem WP_parameter_pop : forall (a:Type), forall (b:Z), forall (rho:(list a)) (rho1:(map Z a)) (rho2:Z) (rho3:Z), ((0%Z < rho2)%Z /\ (buffer_invariant (mk_buffer rho3 rho2 (mk_array b rho1) rho))) -> match rho with | Nil => True | (Cons _ s) => forall (rho4:(list a)), (rho4 = s) -> (((0%Z <= rho3)%Z /\ (rho3 < b)%Z) -> forall (rho5:Z), (rho5 = (rho2 - 1%Z)%Z) -> forall (rho6:Z), (rho6 = (rho3 + 1%Z)%Z) -> ((rho6 = b) -> forall (rho7:Z), (rho7 = 0%Z) -> match rho with | Nil => True | (Cons x l) => ((get rho1 rho3) = x) end)) end. unfold buffer_invariant. unfold get1; simpl. intros a b rho rho1 rho2 rho3 (h1,h2). destruct rho; auto. intros; subst. intuition. generalize (H8 0%Z). ae. Qed.
 (* 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. (* Why3 assumption *) Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. (* Why3 assumption *) Inductive option (a:Type) := | None : option a | Some : a -> option a. Set Contextual Implicit. Implicit Arguments None. Unset Contextual Implicit. Implicit Arguments Some. Parameter nth: forall (a:Type), Z -> (list a) -> (option a). Implicit Arguments nth. Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)), match l with | Nil => ((nth n l) = (None :(option a))) | (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) -> ((nth n l) = (nth (n - 1%Z)%Z r))) end. (* Why3 assumption *) Set Implicit Arguments. Fixpoint length (a:Type)(l:(list a)) {struct l}: Z := match l with