Commit ecd13186 by Jean-Christophe Filliâtre

### FoVeOOS 2011: JC's solutions

parent 12daccee
 (* FoVeOOS 2011 verification competition http://foveoos2011.cost-ic0701.org/verification-competition Challenge 1 *) module Max use import module ref.Refint use import module array.Array let max (a: array int) = { length a > 0 } let x = ref 0 in let y = ref (length a - 1) in while !x <> !y do invariant { 0 <= !x <= !y < length a /\ forall i: int. (0 <= i < !x \/ !y < i < length a) -> (a[i] <= a[!y] \/ a[i] <= a[!x]) } variant { !y - !x } if a[!x] <= a[!y] then incr x else decr y done; !x { 0 <= result < length a /\ forall i: int. 0 <= i < length a -> a[i] <= a[result] } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/foveoos11_challenge1.gui" End: *)
This diff is collapsed.
 (* FoVeOOS 2011 verification competition http://foveoos2011.cost-ic0701.org/verification-competition Challenge 2 *) module MaximumTree use import int.Int use import int.MinMax type tree = Empty | Node tree int tree predicate mem (x: int) (t: tree) = match t with | Empty -> false | Node l v r -> mem x l \/ x = v \/ mem x r end let rec maximum (t: tree) : int = { t <> Empty } match t with | Empty -> absurd | Node Empty v Empty -> v | Node Empty v r -> max v (maximum r) | Node l v Empty -> max (maximum l) v | Node l v r -> max (maximum l) (max v (maximum r)) end { mem result t /\ forall x: int. mem x t -> x <= result } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/foveoos11_challenge2.gui" End: *)

 (* FoVeOOS 2011 verification competition http://foveoos2011.cost-ic0701.org/verification-competition Challenge 3 *) module TwoEqualElements use import module ref.Refint use import module array.Array predicate appear_twice (a: array int) (v: int) (u: int) = exists i: int. 0 <= i < u /\ a[i] = v /\ exists j: int. 0 <= j < u /\ j <> i /\ a[j] = v let two_equal_elements (a: array int) (n: int) = { length a = n+2 /\ n >= 2 /\ (forall i: int. 0 <= i < length a -> 0 <= a[i] < n) /\ exists v1: int. appear_twice a v1 (n+2) /\ exists v2: int. appear_twice a v2 (n+2) /\ v2 <> v1 } let deja_vu = make n False in let v1 = ref (-1) in let v2 = ref (-1) in for i = 0 to n+1 do invariant { (!v1 = -1 -> !v2 = -1) /\ (!v1 <> -1 -> appear_twice a !v1 i) /\ (!v2 <> -1 -> appear_twice a !v2 i /\ !v2 <> !v1) /\ (forall v: int. 0 <= v < n -> if deja_vu[v]=True then exists j: int. 0 <= j < i /\ a[j] = v else forall j: int. 0 <= j < i -> a[j] <> v) /\ (!v1 = -1 -> forall v: int. 0 <= v < n -> not (appear_twice a v i)) /\ (!v2 = -1 -> forall v: int. 0 <= v < n -> v <> !v1 -> not (appear_twice a v i)) } let v = a[i] in if deja_vu[v] then begin if !v1 = -1 then v1 := v else if !v2 = -1 && v <> !v1 then v2 := v end else deja_vu[v] <- True done; (!v1, !v2) { let (v1, v2) = result in appear_twice a v1 (n+2) /\ appear_twice a v2 (n+2) /\ v1 <> v2 } end (* Local Variables: compile-command: "unset LANG; make -C ../.. examples/programs/foveoos11_challenge3.gui" End: *)
 (* 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. Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | (mk_ref contents1) => contents1 end. Implicit Arguments contents. 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). Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. Definition elts (a:Type)(u:(array a)): (map Z a) := match u with | (mk_array _ elts1) => elts1 end. Implicit Arguments elts. Definition length (a:Type)(u:(array a)): Z := match u with | (mk_array length1 _) => length1 end. Implicit Arguments length. Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). Implicit Arguments get1. Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := match a1 with | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v)) end. Implicit Arguments set1. Definition appear_twice(a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z, ((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get1 a i) = v) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get1 a j) = v))). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_two_equal_elements : forall (a:Z), forall (n:Z), forall (a1:(map Z Z)), let a2 := (mk_array a a1) in (((a = (n + 2%Z)%Z) /\ ((2%Z <= n)%Z /\ ((forall (i:Z), ((0%Z <= i)%Z /\ (i < a)%Z) -> ((0%Z <= (get a1 i))%Z /\ ((get a1 i) < n)%Z)) /\ exists v1:Z, (appear_twice a2 v1 (n + 2%Z)%Z) /\ exists v2:Z, (appear_twice a2 v2 (n + 2%Z)%Z) /\ ~ (v2 = v1)))) -> ((0%Z <= n)%Z -> ((0%Z <= (n + 1%Z)%Z)%Z -> forall (v2:Z), forall (v1:Z), forall (deja_vu:(map Z bool)), forall (i:Z), ((0%Z <= i)%Z /\ (i <= (n + 1%Z)%Z)%Z) -> ((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\ (((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\ ((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> (((get deja_vu v) = true) -> exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((get a1 j) = v))) /\ (((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ~ (appear_twice a2 v i)) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v i)))))))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a1 i) in (((0%Z <= result)%Z /\ (result < n)%Z) -> (((get deja_vu result) = true) -> ((v1 = (-1%Z)%Z) -> forall (v11:Z), (v11 = result) -> ((v2 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v11)) -> ~ (appear_twice a2 v (i + 1%Z)%Z))))))))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. intuition. red in H23. destruct H23 as (i0, (h0, (h1, (j, (h2, (h3, h4)))))). subst v11. apply (H4 v); auto. red; exists i0; intuition. assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case. auto. subst i0. unfold get1 in h1; simpl in h1. omega. exists j; intuition. assert (case: (j < i \/ j = i)%Z) by omega. destruct case. auto. subst j. unfold get1 in h4; simpl in h4. omega. 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. Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | (mk_ref contents1) => contents1 end. Implicit Arguments contents. 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). Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. Definition elts (a:Type)(u:(array a)): (map Z a) := match u with | (mk_array _ elts1) => elts1 end. Implicit Arguments elts. Definition length (a:Type)(u:(array a)): Z := match u with | (mk_array length1 _) => length1 end. Implicit Arguments length. Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). Implicit Arguments get1. Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := match a1 with | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v)) end. Implicit Arguments set1. Definition appear_twice(a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z, ((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get1 a i) = v) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get1 a j) = v))). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_two_equal_elements : forall (a:Z), forall (n:Z), forall (a1:(map Z Z)), let a2 := (mk_array a a1) in (((a = (n + 2%Z)%Z) /\ ((2%Z <= n)%Z /\ ((forall (i:Z), ((0%Z <= i)%Z /\ (i < a)%Z) -> ((0%Z <= (get a1 i))%Z /\ ((get a1 i) < n)%Z)) /\ exists v1:Z, (appear_twice a2 v1 (n + 2%Z)%Z) /\ exists v2:Z, (appear_twice a2 v2 (n + 2%Z)%Z) /\ ~ (v2 = v1)))) -> ((0%Z <= n)%Z -> ((0%Z <= (n + 1%Z)%Z)%Z -> forall (v2:Z), forall (v1:Z), forall (deja_vu:(map Z bool)), forall (i:Z), ((0%Z <= i)%Z /\ (i <= (n + 1%Z)%Z)%Z) -> ((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\ (((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\ ((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> (((get deja_vu v) = true) -> exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((get a1 j) = v))) /\ (((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ~ (appear_twice a2 v i)) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v i)))))))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a1 i) in (((0%Z <= result)%Z /\ (result < n)%Z) -> (((get deja_vu result) = true) -> ((~ (v1 = (-1%Z)%Z)) -> ((v2 = (-1%Z)%Z) -> ((result = v1) -> ((v2 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v (i + 1%Z)%Z))))))))))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. intuition. red in H24. destruct H24 as (i0, (h0, (h1, (j, (h2, (h3, h4)))))). apply (H8 v); auto. red; exists i0; intuition. assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case. auto. subst i0. unfold get1 in h1; simpl in h1. omega. exists j; intuition. assert (case: (j < i \/ j = i)%Z) by omega. destruct case. auto. subst j. unfold get1 in h4; simpl in h4. omega. 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. Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | (mk_ref contents1) => contents1 end. Implicit Arguments contents. 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). Inductive array (a:Type) := | mk_array : Z -> (map Z a) -> array a. Implicit Arguments mk_array. Definition elts (a:Type)(u:(array a)): (map Z a) := match u with | (mk_array _ elts1) => elts1 end. Implicit Arguments elts. Definition length (a:Type)(u:(array a)): Z := match u with | (mk_array length1 _) => length1 end. Implicit Arguments length. Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i). Implicit Arguments get1. Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) := match a1 with | (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v)) end. Implicit Arguments set1. Definition appear_twice(a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z, ((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get1 a i) = v) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get1 a j) = v))). (* YOU MAY EDIT THE CONTEXT BELOW *) (* DO NOT EDIT BELOW *) Theorem WP_parameter_two_equal_elements : forall (a:Z), forall (n:Z), forall (a1:(map Z Z)), let a2 := (mk_array a a1) in (((a = (n + 2%Z)%Z) /\ ((2%Z <= n)%Z /\ ((forall (i:Z), ((0%Z <= i)%Z /\ (i < a)%Z) -> ((0%Z <= (get a1 i))%Z /\ ((get a1 i) < n)%Z)) /\ exists v1:Z, (appear_twice a2 v1 (n + 2%Z)%Z) /\ exists v2:Z, (appear_twice a2 v2 (n + 2%Z)%Z) /\ ~ (v2 = v1)))) -> ((0%Z <= n)%Z -> ((0%Z <= (n + 1%Z)%Z)%Z -> forall (v2:Z), forall (v1:Z), forall (deja_vu:(map Z bool)), forall (i:Z), ((0%Z <= i)%Z /\ (i <= (n + 1%Z)%Z)%Z) -> ((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\ (((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\ ((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((get deja_vu v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((get a1 j) = v)) \/ ((~ ((get deja_vu v) = true)) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((get a1 j) = v)))) /\ (((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ~ (appear_twice a2 v i)) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z