Skip to content

GitLab

why3
why3
Commit ebcdf083 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

whyml: require all raised exceptions to be listed 

also, require to list all write/read effects whenever
at least one is listed

fix hashtbl_impl, mergesort_queue, and unraveling_a_card_trick
parent 1245c8f7
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1734 additions and 1417 deletions
CHANGES
View file @ ebcdf083
......@@ -10,6 +10,19 @@ version 0.81, March ??, 2013
o [prover] support for CVC4
o [prover] support for mathematica
o [prover] support for MathSAT5
o [logic] accept type expressions in clone substitutions
o [whyml] support for relation chains (e.g., "e1 = e2 < e3")
* [whyml] every exception raised in a function must be listed
in as "raises { ... }" clause. A postcondition may be omitted
and equals to "true" by default.
* [whyml] if a function definition contains a "writes { ... }"
clause, then every write effect must be listed. If a function
definition contains a "reads { ... }" clause, then every read
_and_ write effect must be listed.
* [drivers] syntax rules, metas, and preludes are inherited
through cloning. Keyword "cloned" becomes unnecessary and
is not accepted anymore.
version 0.80, Oct 31, 2012
==========================
......
examples/hashtbl_impl.mlw
View file @ ebcdf083
......@@ -94,8 +94,7 @@ module HashtblImpl
| None -> forall v: 'a. not (mem (k, v) l)
| Some v -> mem (k, v) l
end }
=
match l with
= match l with
| Nil -> None
| Cons (k', v) r -> if k = k' then Some v else list_find k r
end
......@@ -109,9 +108,8 @@ module HashtblImpl
let rec list_remove (k: key) (l: list (key, 'a)) : list (key, 'a)
variant { l }
ensures { forall k': key, v: 'a.
mem (k',v) result <-> mem (k',v) l /\ k' <> k }
=
match l with
mem (k',v) result <-> mem (k',v) l /\ k' <> k }
= match l with
| Nil -> Nil
| Cons ((k', _) as p) r ->
if k = k' then list_remove k r else Cons p (list_remove k r)
......@@ -121,9 +119,8 @@ module HashtblImpl
writes { h.data.elts, h.view, h.size }
ensures { Map.get h.view k = None }
ensures { forall k': key. k' <> k ->
Map.get h.view k' = Map.get (old h.view) k' }
=
let i = bucket k (length h.data) in
Map.get h.view k' = Map.get (old h.view) k' }
= let i = bucket k (length h.data) in
let l = h.data[i] in
match list_find k l with
| None ->
......@@ -135,12 +132,12 @@ module HashtblImpl
end
let add (h: t 'a) (k: key) (v: 'a) : unit
writes { h.data.elts, h.view, h.size }
writes { h, h.data.elts }
ensures { Map.get h.view k = Some v }
ensures { forall k': key. k' <> k ->
Map.get h.view k' = Map.get (old h.view) k' }
Map.get h.view k' = Map.get (old h.view) k' }
=
abstract if h.size = length h.data then resize h;
abstract (if h.size = length h.data then resize h);
remove h k;
let i = bucket k (length h.data) in
h.data[i] <- Cons (k, v) h.data[i];
......
examples/hashtbl_impl/why3session.xml
View file @ ebcdf083
This diff is collapsed.
examples/mergesort_queue.mlw
View file @ ebcdf083
......@@ -24,15 +24,18 @@ module MergesortQueue
while length q1 > 0 || length q2 > 0 do
invariant { permut (q.elts ++ q1.elts ++ q2.elts)
(at q1.elts 'L ++ at q2.elts 'L) }
variant { length q1.elts + length q2.elts }
variant { length q1 + length q2 }
if length q1 = 0 then
push (pop q2) q
push (safe_pop q2) q
else if length q2 = 0 then
push (pop q1) q
push (safe_pop q1) q
else
let x1 = peek q1 in
let x2 = peek q2 in
if le x1 x2 then push (pop q1) q else push (pop q2) q
let x1 = safe_peek q1 in
let x2 = safe_peek q2 in
if le x1 x2 then
push (safe_pop q1) q
else
push (safe_pop q2) q
done
(*
......
examples/unraveling_a_card_trick/unraveling_a_card_trick_GilbreathCardTrick_WP_parameter_shuffle_1.v → examples/mergesort_queue/mergesort_queue_MergesortQueue_WP_parameter_merge_3.v
View file @ ebcdf083
......@@ -64,86 +64,63 @@ Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) -> exists l1:(list a), exists l2:(list a),
(l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Fixpoint reverse {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: (list
a) :=
Parameter num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
Axiom num_occ_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)),
match l with
| Nil => (Nil :(list a))
| (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil :(list a))))
| Nil => ((num_occ x l) = 0%Z)
| (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
end.
Axiom reverse_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (x:a), ((infix_plpl (reverse (Cons x l1))
l2) = (infix_plpl (reverse l1) (Cons x l2))).
Axiom reverse_reverse : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), ((reverse (reverse l)) = l).
Axiom Mem_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list
a)), (mem x l) <-> (0%Z < (num_occ x l))%Z.
Axiom Reverse_length : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length (reverse l)) = (length l)).
Axiom Append_Num_Occ : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x
l1) + (num_occ x l2))%Z).
(* Why3 assumption *)
Inductive option
(a:Type) {a_WT:WhyType a} :=
| None : option a
| Some : a -> option a.
Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a).
Existing Instance option_WhyType.
Implicit Arguments None [[a] [a_WT]].
Implicit Arguments Some [[a] [a_WT]].
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a)) (l2:(list
a)): Prop := forall (x:a), ((num_occ x l1) = (num_occ x l2)).
Parameter nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) -> (option a).
Axiom Permut_refl : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
(permut l l).
Axiom nth_def : forall {a:Type} {a_WT:WhyType a}, 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.
Axiom Permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> (permut l2 l1).
Parameter m: Z.
Axiom Permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut
l1 l3)).
Axiom m_positive : (0%Z < m)%Z.
Axiom Permut_cons : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)).
Parameter n: Z.
Axiom Permut_swap : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(l:(list a)), (permut (Cons x (Cons y l)) (Cons y (Cons x l))).
Axiom n_nonnegative : (0%Z <= n)%Z.
Axiom Permut_cons_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(l1:(list a)) (l2:(list a)), (permut (infix_plpl (Cons x l1) l2)
(infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Inductive shuffle{a:Type} {a_WT:WhyType a} : (list a) -> (list a) -> (list
a) -> Prop :=
| Shuffle_nil_left : forall (l:(list a)), (shuffle l (Nil :(list a)) l)
| Shuffle_nil_right : forall (l:(list a)), (shuffle (Nil :(list a)) l l)
| Shuffle_cons_left : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list a)),
(shuffle a1 b c) -> (shuffle (Cons x a1) b (Cons x c))
| Shuffle_cons_right : forall (x:a) (a1:(list a)) (b:(list a)) (c:(list
a)), (shuffle a1 b c) -> (shuffle a1 (Cons x b) (Cons x c)).
Axiom Permut_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3)
(infix_plpl l1 (infix_plpl l2 l3))).
Axiom shuffle_nil_nil_nil : forall {a:Type} {a_WT:WhyType a}, (shuffle
(Nil :(list a)) (Nil :(list a)) (Nil :(list a))).
Axiom Permut_append : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2
k2) -> (permut (infix_plpl l1 l2) (infix_plpl k1 k2))).
Axiom shuffle_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(list a))
(b:(list a)) (c:(list a)), (shuffle a1 b c) -> (shuffle b a1 c).
Axiom Permut_append_swap : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
a)) (l2:(list a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)).
Axiom shuffle_length : forall {a:Type} {a_WT:WhyType a}, forall (a1:(list a))
(b:(list a)) (c:(list a)), (shuffle a1 b c) ->
(((length a1) + (length b))%Z = (length c)).
Axiom Permut_mem : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list
a)) (l2:(list a)), (permut l1 l2) -> ((mem x l1) -> (mem x l2)).
(* Why3 assumption *)
Definition suit_ordered (l:(list Z)): Prop := forall (i:Z) (j:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < m)%Z) ->
((nth ((i * m)%Z + j)%Z l) = (Some j))).
(* Why3 assumption *)
Definition suit_sorted (l:(list Z)): Prop := (forall (i:Z) (v:Z), ((nth i
l) = (Some v)) -> ((0%Z <= v)%Z /\ (v < m)%Z)) /\ forall (i:Z) (j1:Z)
(j2:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j1)%Z /\ (j1 < m)%Z) ->
(((0%Z <= j2)%Z /\ (j2 < m)%Z) -> ~ ((nth ((i * m)%Z + j1)%Z
l) = (nth ((i * m)%Z + j2)%Z l)))).
Axiom gilbreath_card_trick : forall (a:(list Z)), ((length a) = (n * m)%Z) ->
((suit_ordered a) -> forall (c:(list Z)) (d:(list Z)), (a = (infix_plpl c
d)) -> forall (b:(list Z)), (shuffle c (reverse d) b) -> (suit_sorted b)).
Axiom Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), (permut l1 l2) -> ((length l1) = (length l2)).
(* Why3 assumption *)
Inductive t (a:Type) {a_WT:WhyType a} :=
......@@ -159,31 +136,65 @@ Definition elts {a:Type} {a_WT:WhyType a} (v:(t a)): (list a) :=
end.
(* Why3 assumption *)
Definition length1 {a:Type} {a_WT:WhyType a} (s:(t a)): Z :=
(length (elts s)).
Definition length1 {a:Type} {a_WT:WhyType a} (q:(t a)): Z :=
(length (elts q)).
Axiom elt : Type.
Parameter elt_WhyType : WhyType elt.
Existing Instance elt_WhyType.
Parameter le: elt -> elt -> Prop.
Require Import Why3.
Axiom total_preorder1 : forall (x:elt) (y:elt), (le x y) \/ (le y x).
Axiom total_preorder2 : forall (x:elt) (y:elt) (z:elt), (le x y) -> ((le y
z) -> (le x z)).
(* Why3 assumption *)
Inductive sorted : (list elt) -> Prop :=
| Sorted_Nil : (sorted (Nil :(list elt)))
| Sorted_One : forall (x:elt), (sorted (Cons x (Nil :(list elt))))
| Sorted_Two : forall (x:elt) (y:elt) (l:(list elt)), (le x y) -> ((sorted
(Cons y l)) -> (sorted (Cons x (Cons y l)))).
Axiom sorted_mem : forall (x:elt) (l:(list elt)), ((forall (y:elt), (mem y
l) -> (le x y)) /\ (sorted l)) <-> (sorted (Cons x l)).
(* Why3 goal *)
Theorem WP_parameter_shuffle : forall (b:(list Z)) (a:(list Z)),
forall (c:(list Z)), (c = (Nil :(list Z))) -> forall (c1:(list Z))
(b1:(list Z)) (a1:(list Z)), (exists a':(list Z), (exists b':(list Z),
((reverse a) = (infix_plpl (reverse a1) a')) /\
(((reverse b) = (infix_plpl (reverse b1) b')) /\ (shuffle a' b' c1)))) ->
forall (result:bool), ((result = true) <-> (a1 = (Nil :(list Z)))) ->
((~ (result = true)) -> forall (o:bool), ((o = true) <-> (a1 = (Nil :(list
Z)))) -> ((~ (o = true)) -> forall (result1:bool), ((result1 = true) <->
(b1 = (Nil :(list Z)))) -> ((result1 = true) -> forall (a2:(list Z)),
forall (o1:Z),
match a1 with
Theorem WP_parameter_merge : forall (q:(list elt)) (q2:(list elt)) (q1:(list
elt)), (q = (Nil :(list elt))) -> forall (q3:(list elt)) (q21:(list elt))
(q11:(list elt)), (permut (infix_plpl (infix_plpl q3 q11) q21)
(infix_plpl q1 q2)) -> ((0%Z < (length q11))%Z ->
((~ ((length q11) = 0%Z)) -> ((~ ((length q21) = 0%Z)) ->
((~ (q11 = (Nil :(list elt)))) -> forall (x1:elt),
match q11 with
| Nil => False
| (Cons x _) => (x1 = x)
end -> ((~ (q21 = (Nil :(list elt)))) -> forall (x2:elt),
match q21 with
| Nil => False
| (Cons x _) => (x2 = x)
end -> ((~ (le x1 x2)) -> ((~ (q21 = (Nil :(list elt)))) ->
forall (q22:(list elt)), forall (o:elt),
match q21 with
| Nil => False
| (Cons x t1) => (o1 = x) /\ (a2 = t1)
end -> forall (c2:(list Z)), (c2 = (Cons o1 c1)) -> exists a':(list Z),
exists b':(list Z), ((reverse a) = (infix_plpl (reverse a2) a')) /\
(((reverse b) = (infix_plpl (reverse b1) b')) /\ (shuffle a' b' c2))))).
intros b a c h1 c1 b1 a1 (a',(b',(h2,(h3,h4)))) result h5 h6 o h7 h8 result1
h9 h10 a2 o1 h11 c2 h12.
exists (Cons o1 a'); exists b'; why3 "Alt-Ergo,0.95.1,".
| (Cons x t1) => (o = x) /\ (q22 = t1)
end -> forall (q4:(list elt)), (q4 = (infix_plpl q3 (Cons o (Nil :(list
elt))))) -> (permut (infix_plpl (infix_plpl q4 q11) q22) (infix_plpl q1
q2))))))))).
(* Why3 intros q q2 q1 h1 q3 q21 q11 h2 h3 h4 h5 h6 x1 h7 h8 x2 h9 h10 h11
q22 o h12 q4 h13. *)
intros q q2 q1 h1 q3 q21 q11 h2 h3 h4 h5 h6 x1 h7 x2 h8 h9 q22 o h10
q4 h11.
destruct q21.
elim h9.
intuition; subst.
apply Permut_trans with (infix_plpl (infix_plpl q3 q11) (Cons e q21)); auto.
repeat rewrite <- Append_assoc.
eapply Permut_append; auto.
apply Permut_refl.
simpl.
apply Permut_cons_append.
Qed.
examples/mergesort_queue/mergesort_queue_WP_MergesortQueue_WP_parameter_merge_1.v deleted 100644 → 0
View file @ 1245c8f7
(* 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 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))).
(* 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))).
Parameter num_occ: forall (a:Type), a -> (list a) -> Z.
Implicit Arguments num_occ.
Axiom num_occ_def : forall (a:Type), forall (x:a) (l:(list a)),
match l with
| Nil => ((num_occ x l) = 0%Z)
| (Cons y r) => ((x = y) -> ((num_occ x l) = (1%Z + (num_occ x r))%Z)) /\
((~ (x = y)) -> ((num_occ x l) = (0%Z + (num_occ x r))%Z))
end.
Axiom Mem_Num_Occ : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) <->
(0%Z < (num_occ x l))%Z.
Axiom Append_Num_Occ : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
a)), ((num_occ x (infix_plpl l1 l2)) = ((num_occ x l1) + (num_occ x
l2))%Z).
(* Why3 assumption *)
Definition permut (a:Type)(l1:(list a)) (l2:(list a)): Prop := forall (x:a),
((num_occ x l1) = (num_occ x l2)).
Implicit Arguments permut.
Axiom Permut_refl : forall (a:Type), forall (l:(list a)), (permut l l).
Axiom Permut_sym : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> (permut l2 l1).
Axiom Permut_trans : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), (permut l1 l2) -> ((permut l2 l3) -> (permut l1 l3)).
Axiom Permut_cons : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list
a)), (permut l1 l2) -> (permut (Cons x l1) (Cons x l2)).
Axiom Permut_swap : forall (a:Type), forall (x:a) (y:a) (l:(list a)),
(permut (Cons x (Cons y l)) (Cons y (Cons x l))).
Axiom Permut_cons_append : forall (a:Type), forall (x:a) (l1:(list a))
(l2:(list a)), (permut (infix_plpl (Cons x l1) l2) (infix_plpl l1 (Cons x
l2))).
Axiom Permut_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(l3:(list a)), (permut (infix_plpl (infix_plpl l1 l2) l3) (infix_plpl l1
(infix_plpl l2 l3))).
Axiom Permut_append : forall (a:Type), forall (l1:(list a)) (l2:(list a))
(k1:(list a)) (k2:(list a)), (permut l1 k1) -> ((permut l2 k2) ->
(permut (infix_plpl l1 l2) (infix_plpl k1 k2))).
Axiom Permut_append_swap : forall (a:Type), forall (l1:(list a)) (l2:(list
a)), (permut (infix_plpl l1 l2) (infix_plpl l2 l1)).
Axiom Permut_mem : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> ((mem x l1) -> (mem x l2)).
Axiom Permut_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
(permut l1 l2) -> ((length l1) = (length l2)).
(* Why3 assumption *)
Inductive t (a:Type) :=
| mk_t : (list a) -> t a.
Implicit Arguments mk_t.
(* Why3 assumption *)
Definition elts (a:Type)(v:(t a)): (list a) :=
match v with
| (mk_t x) => x
end.
Implicit Arguments elts.
Parameter elt : Type.
Parameter le: elt -> elt -> Prop.
Axiom total_preorder1 : forall (x:elt) (y:elt), (le x y) \/ (le y x).
Axiom total_preorder2 : forall (x:elt) (y:elt) (z:elt), (le x y) -> ((le y
z) -> (le x z)).
(* Why3 assumption *)
Inductive sorted : (list elt) -> Prop :=
| Sorted_Nil : (sorted (Nil :(list elt)))
| Sorted_One : forall (x:elt), (sorted (Cons x (Nil :(list elt))))
| Sorted_Two : forall (x:elt) (y:elt) (l:(list elt)), (le x y) ->
((sorted (Cons y l)) -> (sorted (Cons x (Cons y l)))).
Axiom sorted_mem : forall (x:elt) (l:(list elt)), ((forall (y:elt), (mem y
l) -> (le x y)) /\ (sorted l)) <-> (sorted (Cons x l)).
(* Why3 goal *)
Theorem WP_parameter_merge : forall (q:(list elt)) (q2:(list elt)) (q1:(list
elt)), (q = (Nil :(list elt))) -> forall (q3:(list elt)) (q21:(list elt))
(q11:(list elt)), (permut (infix_plpl (infix_plpl q3 q11) q21)
(infix_plpl q1 q2)) -> ((0%Z < (length q11))%Z ->
((~ ((length q11) = 0%Z)) -> ((~ ((length q21) = 0%Z)) -> forall (x1:elt),
match q11 with
| Nil => False
| (Cons x _) => (x1 = x)
end -> forall (x2:elt),
match q21 with
| Nil => False
| (Cons x _) => (x2 = x)
end -> ((~ (le x1 x2)) -> forall (q22:(list elt)), forall (o:elt),
match q21 with
| Nil => False
| (Cons x t1) => (o = x) /\ (q22 = t1)
end -> forall (q4:(list elt)), (q4 = (infix_plpl q3 (Cons o (Nil :(list
elt))))) -> (permut (infix_plpl (infix_plpl q4 q11) q22) (infix_plpl q1
q2)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
destruct q21.
elim H7.
intuition; subst.
clear H1 H2 H3 H4 H6.
apply Permut_trans with (infix_plpl (infix_plpl q3 q11) (Cons e q21)); auto.
repeat rewrite <- Append_assoc.
eapply Permut_append; auto.
apply Permut_refl.
simpl.
apply Permut_cons_append.
Qed.
examples/mergesort_queue/why3session.xml
View file @ ebcdf083
This diff is collapsed.
examples/unraveling_a_card_trick.mlw
View file @ ebcdf083
......@@ -74,18 +74,20 @@ module GilbreathCardTrick
shuffle (reverse (old a.elts)) (reverse (old b.elts)) result.elts }
= 'Init:
let c = create () in
let ghost a' = create () in
let ghost b' = create () in
while not (is_empty a && is_empty b) do
invariant {
exists a' b': list int.
reverse (at a.elts 'Init) = reverse a.elts ++ a' /\
reverse (at b.elts 'Init) = reverse b.elts ++ b' /\
shuffle a' b' c.elts
}
variant { length a + length b }
if not (is_empty a) && (is_empty b || any bool) then
push (pop a) c
else
push (pop b) c
invariant { reverse (at a.elts 'Init) = reverse a.elts ++ a'.elts }
invariant { reverse (at b.elts 'Init) = reverse b.elts ++ b'.elts }
invariant { shuffle a'.elts b'.elts c.elts }
variant { length a + length b }
if not (is_empty a) && (is_empty b || any bool) then begin
ghost (push (safe_top a) a');
push (safe_pop a) c
end else begin
ghost (push (safe_top b) b');
push (safe_pop b) c
end
done;
c
......@@ -99,7 +101,7 @@ module GilbreathCardTrick
for i = 1 to cut do
invariant { length a = n*m-i+1 /\ length d_ = i-1 /\
at a.elts 'Init = reverse d_.elts ++ a.elts }
push (pop a) d_
push (safe_pop a) d_
done;
assert { at a.elts 'Init = reverse d_.elts ++ a.elts };
(* then suffle c (that is a) and d_ to get b *)
......
examples/unraveling_a_card_trick/unraveling_a_card_trick_WP_GilbreathCardTrick_WP_parameter_card_trick_1.v deleted 100644 → 0
View file @ 1245c8f7
(* 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.