Commit 0ba85a84 by Jean-Christophe Filliâtre

### vstte12_ring_buffer_2 -> vstte12_ring_buffer

parent 81bc5393
 ... ... @@ -3,19 +3,32 @@ https://sites.google.com/site/vstte2012/compet Problem 3: Queue data structure implemented using a ring buffer *) 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.List use import list.Append use import list.NthLengthAppend as L use import array.Array type buffer 'a = { mutable first: int; mutable len : int; data : array 'a; ghost mutable sequence: list 'a; } invariant { let size = Array.length self.data in 0 <= self.first < size /\ 0 <= self.len <= size /\ self.len = L.length self.sequence /\ forall i: int. 0 <= i < self.len -> (self.first + i < size -> nth i self.sequence = Some self.data[self.first + i]) /\ (0 <= self.first + i - size -> nth i self.sequence = Some self.data[self.first + i - size]) } (* total capacity of the buffer *) ... ... @@ -24,90 +37,45 @@ module RingBuffer (* 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 (* the model of a buffer is a list of elements *) function sequence (b: buffer 'a) : list 'a axiom sequence_def_1: forall b: buffer 'a. buffer_invariant b -> b.len = 0 -> sequence b = Nil axiom sequence_def_2: forall b: buffer 'a. buffer_invariant b -> b.len > 0 -> b.first+1 < size b -> sequence b = Cons b.data[b.first] (sequence { b with first = b.first+1; len = b.len-1 }) axiom sequence_def_3: forall b: buffer 'a. buffer_invariant b -> b.len > 0 -> b.first+1 = size b -> sequence b = Cons b.data[b.first] (sequence { b with first = 0; len = b.len-1 }) lemma sequence_ind_1: forall b: buffer 'a. buffer_invariant b -> b.len > 0 -> b.first+b.len-1 < size b -> sequence b = sequence { b with first = b.first; len = b.len-1 } ++ Cons b.data[b.first+b.len-1] Nil lemma sequence_ind_2: forall b: buffer 'a. buffer_invariant b -> b.len > 0 -> b.first+b.len-1 >= size b -> sequence b = sequence { b with first = b.first; len = b.len-1 } ++ Cons b.data[b.first+b.len-1 - size b] Nil lemma sequence_invariance: forall b1 b2: buffer 'a. buffer_invariant b1 -> buffer_invariant b2 -> b1.first = b2.first -> b1.len = b2.len -> size b1 = size b2 -> (forall i: int. b1.first <= i < b1.first+b1.len -> i < size b1 -> b1.data[i] = b2.data[i]) -> (forall i: int. 0 <= i < b1.first+b1.len - size b1 -> b1.data[i] = b2.data[i]) -> sequence b1 = sequence b2 (* code *) let create (n: int) (dummy: 'a) requires { n > 0 } ensures { buffer_invariant result /\ size result = n /\ sequence result = Nil } = { first = 0; len = 0; data = make n dummy; } ensures { size result = n /\ result.sequence = Nil } = { first = 0; len = 0; data = make n dummy; sequence = Nil } let length (b: buffer 'a) requires { buffer_invariant b } ensures { result = length b } = b.len let clear (b: buffer 'a) requires { buffer_invariant b } ensures { buffer_invariant b /\ length b = 0 /\ sequence b = Nil } = b.len <- 0 ensures { length b = 0 /\ b.sequence = Nil } = ghost b.sequence <- Nil; b.len <- 0 let push (b: buffer 'a) (x: 'a) requires { length b < size b /\ buffer_invariant b } ensures { buffer_invariant b /\ length b = (old (length b)) + 1 /\ sequence b = (old (sequence b)) ++ Cons x Nil } = let i = b.first + b.len in requires { length b < size b } ensures { length b = (old (length b)) + 1 /\ b.sequence = (old b.sequence) ++ Cons x Nil } = 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 let head (b: buffer 'a) requires { length b > 0 /\ buffer_invariant b } ensures { match sequence b with Nil -> false | Cons x _ -> result = x end } requires { length b > 0 } ensures { match b.sequence with Nil -> false | Cons x _ -> result = x end } = b.data[b.first] let pop (b: buffer 'a) requires { length b > 0 /\ buffer_invariant b } ensures { buffer_invariant b /\ length b = (old (length b)) - 1 /\ match old (sequence b) with requires { length b > 0 } ensures { length b = (old (length b)) - 1 /\ match old b.sequence with | Nil -> false | Cons x l -> result = x /\ sequence b = l end } = let r = b.data[b.first] in | Cons x l -> result = x /\ b.sequence = l end } = 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; ... ...
 (* 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 qtmark : Type. Parameter at1: forall (a:Type), a -> qtmark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. (* 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 *) 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). (* 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 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))). 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). (* 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) -> buffer a. Implicit Arguments mk_buffer. (* Why3 assumption *) Definition data (a:Type)(v:(buffer a)): (array a) := match v with | (mk_buffer x x1 x2) => x2 end. Implicit Arguments data. (* Why3 assumption *) Definition len (a:Type)(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2) => x1 end. Implicit Arguments len. (* Why3 assumption *) Definition first (a:Type)(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2) => 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). Implicit Arguments buffer_invariant. Parameter sequence: forall (a:Type), (buffer a) -> (list a). Implicit Arguments sequence. Axiom sequence_def_1 : forall (a:Type), forall (b:(buffer a)), (buffer_invariant b) -> (((len b) = 0%Z) -> ((sequence b) = (Nil :(list a)))). Axiom sequence_def_2 : forall (a:Type), forall (b:(buffer a)), (buffer_invariant b) -> ((0%Z < (len b))%Z -> ((((first b) + 1%Z)%Z < (size b))%Z -> ((sequence b) = (Cons (get1 (data b) (first b)) (sequence (mk_buffer ((first b) + 1%Z)%Z ((len b) - 1%Z)%Z (data b))))))). Axiom sequence_def_3 : forall (a:Type), forall (b:(buffer a)), (buffer_invariant b) -> ((0%Z < (len b))%Z -> ((((first b) + 1%Z)%Z = (size b)) -> ((sequence b) = (Cons (get1 (data b) (first b)) (sequence (mk_buffer 0%Z ((len b) - 1%Z)%Z (data b))))))). Axiom sequence_ind_1 : forall (a:Type), forall (b:(buffer a)), (buffer_invariant b) -> ((0%Z < (len b))%Z -> (((((first b) + (len b))%Z - 1%Z)%Z < (size b))%Z -> ((sequence b) = (infix_plpl (sequence (mk_buffer (first b) ((len b) - 1%Z)%Z (data b))) (Cons (get1 (data b) (((first b) + (len b))%Z - 1%Z)%Z) (Nil :(list a))))))). Axiom sequence_ind_2 : forall (a:Type), forall (b:(buffer a)), (buffer_invariant b) -> ((0%Z < (len b))%Z -> (((size b) <= (((first b) + (len b))%Z - 1%Z)%Z)%Z -> ((sequence b) = (infix_plpl (sequence (mk_buffer (first b) ((len b) - 1%Z)%Z (data b))) (Cons (get1 (data b) ((((first b) + (len b))%Z - 1%Z)%Z - (size b))%Z) (Nil :(list a))))))). Axiom sequence_invariance : forall (a:Type), forall (b1:(buffer a)) (b2:(buffer a)), (buffer_invariant b1) -> ((buffer_invariant b2) -> (((first b1) = (first b2)) -> (((len b1) = (len b2)) -> (((size b1) = (size b2)) -> ((forall (i:Z), (((first b1) <= i)%Z /\ (i < ((first b1) + (len b1))%Z)%Z) -> ((i < (size b1))%Z -> ((get1 (data b1) i) = (get1 (data b2) i)))) -> ((forall (i:Z), ((0%Z <= i)%Z /\ (i < (((first b1) + (len b1))%Z - (size b1))%Z)%Z) -> ((get1 (data b1) i) = (get1 (data b2) i))) -> ((sequence b1) = (sequence b2)))))))). (* Why3 goal *) Theorem WP_parameter_harness : (0%Z < 10%Z)%Z -> forall (result:Z) (result1:Z) (result2:Z) (result3:(map Z Z)), let result4 := (mk_buffer result result1 (mk_array result2 result3)) in (((buffer_invariant result4) /\ ((result2 = 10%Z) /\ ((sequence result4) = (Nil :(list Z))))) -> (((result1 < result2)%Z /\ (buffer_invariant result4)) -> forall (fresh:(map Z Z)), forall (fresh1:Z), let b := (mk_buffer result fresh1 (mk_array result2 fresh)) in (((buffer_invariant b) /\ ((fresh1 = (result1 + 1%Z)%Z) /\ ((sequence b) = (infix_plpl (sequence result4) (Cons 1%Z (Nil :(list Z))))))) -> (((fresh1 < result2)%Z /\ (buffer_invariant b)) -> forall (fresh2:(map Z Z)), forall (fresh3:Z), let b1 := (mk_buffer result fresh3 (mk_array result2 fresh2)) in (((buffer_invariant b1) /\ ((fresh3 = (fresh1 + 1%Z)%Z) /\ ((sequence b1) = (infix_plpl (sequence b) (Cons 2%Z (Nil :(list Z))))))) -> (((fresh3 < result2)%Z /\ (buffer_invariant b1)) -> forall (fresh4:(map Z Z)), forall (fresh5:Z), let b2 := (mk_buffer result fresh5 (mk_array result2 fresh4)) in (((buffer_invariant b2) /\ ((fresh5 = (fresh3 + 1%Z)%Z) /\ ((sequence b2) = (infix_plpl (sequence b1) (Cons 3%Z (Nil :(list Z))))))) -> (((0%Z < fresh5)%Z /\ (buffer_invariant b2)) -> forall (fresh6:Z), forall (fresh7:Z), let b3 := (mk_buffer fresh7 fresh6 (mk_array result2 fresh4)) in forall (result5:Z), ((buffer_invariant b3) /\ ((fresh6 = (fresh5 - 1%Z)%Z) /\ match (sequence b2) with | Nil => False | (Cons x l) => (result5 = x) /\ ((sequence b3) = l) end)) -> ((result5 = 1%Z) -> (((0%Z < fresh6)%Z /\ (buffer_invariant b3)) -> forall (fresh8:Z), forall (fresh9:Z), let b4 := (mk_buffer fresh9 fresh8 (mk_array result2 fresh4)) in forall (result6:Z), ((buffer_invariant b4) /\ ((fresh8 = (fresh6 - 1%Z)%Z) /\ match (sequence b3) with | Nil => False | (Cons x l) => (result6 = x) /\ ((sequence b4) = l) end)) -> (result6 = 2%Z))))))))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. intuition. subst. clear H2 H4 H7 H9 H12 H14 H17 H19 H23 H25 H27. rewrite H5 in *; clear H5. rewrite H10 in *; clear H10. rewrite H15 in *; clear H15. rewrite H20 in *; clear H20. simpl in H26. destruct H26. rewrite H2 in *; clear H2. intuition. 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 *) 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). (* 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 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))). 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) -> buffer a. Implicit Arguments mk_buffer. (* Why3 assumption *) Definition data (a:Type)(v:(buffer a)): (array a) := match v with | (mk_buffer x x1 x2) => x2