Skip to content

GitLab

why3
why3
Commit fc7e0b73 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

selection sort now proved automatically (thanks, Claude)

parent 443fb598
Hide whitespace changes
Inline Side-by-side
Showing with 47 additions and 206 deletions
examples/programs/selection_sort.mlw
View file @ fc7e0b73
......@@ -31,7 +31,9 @@ module Quicksort
{ i <= !min < j && forall k: int. i <= k < j -> a[!min] <= a[k] }
if a[j] < a[!min] then min := j
done;
if !min <> i then swap a !min i
label L1:
if !min <> i then swap a !min i;
assert { permut a (at a L1) }
done
{ sorted a and permut a (old a) }
......
examples/programs/selection_sort/selection_sort.mlw_Quicksort_WP_parameter selection_sort_2.v deleted 100644 → 0
View file @ 443fb598
(* 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 label : Type.
Parameter at1: forall (a:Type), a -> label -> 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 sorted_sub(a:(map Z Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z),
(((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> ((get a i1) <= (get a
i2))%Z.
Definition sorted_sub1(a:(array Z)) (l:Z) (u:Z): Prop := (sorted_sub (elts a)
l u).
Definition sorted(a:(array Z)): Prop := (sorted_sub (elts a) 0%Z (length a)).
Definition map_eq_sub (a:Type)(a1:(map Z a)) (a2:(map Z a)) (l:Z)
(u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1
i) = (get a2 i)).
Implicit Arguments map_eq_sub.
Definition exchange (a:Type)(a1:(map Z a)) (a2:(map Z a)) (i:Z)
(j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\
forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))).
Implicit Arguments exchange.
Axiom exchange_set : forall (a:Type), forall (a1:(map Z a)), forall (i:Z)
(j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i j).
Inductive permut_sub{a:Type} : (map Z a) -> (map Z a) -> Z -> Z -> Prop :=
| permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u)
| permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u)
| permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l
u) -> (permut_sub a1 a3 l u))
| permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z)
(u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\
(j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))).
Implicit Arguments permut_sub.
Axiom permut_weakening : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z
a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\
(r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
Axiom permut_eq : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (l <= u)%Z -> ((permut_sub a1 a2 l u) -> forall (i:Z),
((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i))).
Axiom permut_exists : forall (a:Type), forall (a1:(map Z a)) (a2:(map Z a)),
forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\
(i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2
i) = (get a1 j)).
Definition exchange1 (a:Type)(a1:(array a)) (a2:(array a)) (i:Z)
(j:Z): Prop := (exchange (elts a1) (elts a2) i j).
Implicit Arguments exchange1.
Definition permut_sub1 (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (permut_sub (elts a1) (elts a2) l u).
Implicit Arguments permut_sub1.
Definition permut (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (permut_sub (elts a1) (elts a2) 0%Z
(length a1)).
Implicit Arguments permut.
Axiom exchange_permut : forall (a:Type), forall (a1:(array a)) (a2:(array a))
(i:Z) (j:Z), (exchange1 a1 a2 i j) -> (((length a1) = (length a2)) ->
(((0%Z <= i)%Z /\ (i < (length a1))%Z) -> (((0%Z <= j)%Z /\
(j < (length a1))%Z) -> (permut a1 a2)))).
Definition array_eq_sub (a:Type)(a1:(array a)) (a2:(array a)) (l:Z)
(u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u).
Implicit Arguments array_eq_sub.
Definition array_eq (a:Type)(a1:(array a)) (a2:(array a)): Prop :=
((length a1) = (length a2)) /\ (array_eq_sub a1 a2 0%Z (length a1)).
Implicit Arguments array_eq.
Axiom array_eq_sub_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)) (l:Z) (u:Z), (array_eq_sub a1 a2 l u) -> (permut_sub1 a1 a2 l u).
Axiom array_eq_permut : forall (a:Type), forall (a1:(array a)) (a2:(array
a)), (array_eq a1 a2) -> (permut a1 a2).
Theorem WP_parameter_selection_sort : forall (a:Z), forall (a1:(map Z Z)),
let a2 := (mk_array a a1) in ((0%Z <= (a - 1%Z)%Z)%Z -> forall (a3:(map Z
Z)), forall (i:Z), ((0%Z <= i)%Z /\ (i <= (a - 1%Z)%Z)%Z) ->
(((sorted_sub a3 0%Z i) /\ ((permut (mk_array a a3) a2) /\ forall (k1:Z)
(k2:Z), ((((0%Z <= k1)%Z /\ (k1 < i)%Z) /\ (i <= k2)%Z) /\ (k2 < a)%Z) ->
((get a3 k1) <= (get a3 k2))%Z)) -> (((i + 1%Z)%Z <= (a - 1%Z)%Z)%Z ->
forall (min:Z), (((i <= min)%Z /\ (min < ((a - 1%Z)%Z + 1%Z)%Z)%Z) /\
forall (k:Z), ((i <= k)%Z /\ (k < ((a - 1%Z)%Z + 1%Z)%Z)%Z) -> ((get a3
min) <= (get a3 k))%Z) -> ((~ (min = i)) -> ((((0%Z <= min)%Z /\
(min < a)%Z) /\ ((0%Z <= i)%Z /\ (i < a)%Z)) -> forall (a4:(map Z Z)),
(exchange a4 a3 min i) -> (permut (mk_array a a4) a2)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
unfold permut; simpl; intuition.
apply permut_trans with a3; auto.
apply permut_exchange with min i; auto.
unfold permut in H1.
intuition.
Qed.
(* DO NOT EDIT BELOW *)
examples/programs/selection_sort/why3session.xml
View file @ fc7e0b73
......@@ -8,7 +8,7 @@
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort" expl="correctness of parameter selection_sort" sum="e8a4794296a922d59fe66c64846145e7" proved="true" expanded="true">
<goal name="WP_parameter selection_sort" expl="correctness of parameter selection_sort" sum="fe1cd1b47feeb0ae3809694b5181ee80" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.1" expl="normal postcondition" sum="2b0c2302cfdd16f5a6458e573ee4929f" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......@@ -20,84 +20,104 @@
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3" expl="for loop preservation" sum="e400d0f5646ca3df76c127eaacaa6a05" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3" expl="for loop preservation" sum="eb5013c23f31c134ba08ca062686984e" proved="true" expanded="true">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.1" expl="for loop preservation" sum="ba14d9e56be4df6a4857c6e4bd546186" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.2" expl="for loop preservation" sum="e77211a251b0e3f51c3ea7fe0ed1d77d" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.2" expl="for loop preservation" sum="00466a01789dab2720a99ca89698bd39" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.3" expl="for loop preservation" sum="7d58315ddce9b12a7c79577be170ef37" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.3" expl="for loop preservation" sum="c707491be4ab5917899db51764de68a9" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.4" expl="for loop preservation" sum="67766e474e216c1654a4833edfdc1ff8" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.4" expl="for loop preservation" sum="65a04c15b9c186e076799133e97990c7" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.5" expl="for loop preservation" sum="acc4af5680328618751e3115eb0cafa8" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.5" expl="for loop preservation" sum="1088f3648ec0c396ee78bfa66461c2c2" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.6" expl="for loop preservation" sum="6fa1119b7f2189d92313c6ad2d965d11" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.6" expl="for loop preservation" sum="48e51c862477d9b9bb7d9949ba1d7622" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.7" expl="for loop preservation" sum="83a18eca4d563c48415c64e222c61a2a" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.7" expl="for loop preservation" sum="f16e3d3731417a5ba19f3c0e905a35d7" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.8" expl="for loop preservation" sum="663cc124cde1784b5df9d1726248f0f0" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.9" expl="for loop preservation" sum="5914e160c4b2042d8ea1ec0cfa66b855" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.8" expl="for loop preservation" sum="aa1e8d1771330da0b312586be8b12fca" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.10" expl="for loop preservation" sum="aa1e8d1771330da0b312586be8b12fca" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.9" expl="for loop preservation" sum="148822fa93fae4de0add9ab295d0002d" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.11" expl="for loop preservation" sum="148822fa93fae4de0add9ab295d0002d" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.10" expl="for loop preservation" sum="eab8745b368bae03988bac1294dc158f" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.12" expl="for loop preservation" sum="eab8745b368bae03988bac1294dc158f" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.11" expl="for loop preservation" sum="419de9794f1c2df8155a93aef6f4e1c7" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.13" expl="for loop preservation" sum="8c5db9d37ed048e705792760575cd7c1" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
<result status="valid" time="2.42"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.12" expl="for loop preservation" sum="b0f85fac59f0d82b1a79418a81d6dd3d" proved="true" expanded="true">
<proof prover="coq" timelimit="10" edited="selection_sort.mlw_Quicksort_WP_parameter selection_sort_2.v" obsolete="false">
<result status="valid" time="0.64"/>
<goal name="WP_parameter selection_sort.3.14" expl="for loop preservation" sum="93854214f1088a4e0917e0fa83e10b35" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.13"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.13" expl="for loop preservation" sum="4c721389c01b52a499179fc4559a84ae" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.15" expl="for loop preservation" sum="fa0684d84aa66def1fb43b34cdead866" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.14" expl="for loop preservation" sum="fed0a7cebdfc18eeb8bb8a50b66c52a2" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.16" expl="for loop preservation" sum="862b60c702f220d485e30f4ca674ac3b" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.15" expl="for loop preservation" sum="22e3ee5ad3f3b34e7b49a3f7ec47a13d" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.17" expl="for loop preservation" sum="1e3c5b5646a30d3cb0df12fdaa23603a" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.16" expl="for loop preservation" sum="00e74c846e5cbce19d3e955219dc1d61" proved="true" expanded="true">
<goal name="WP_parameter selection_sort.3.18" expl="for loop preservation" sum="bc71a112cc02c7096c0de72bd7b7ef9e" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.19" expl="for loop preservation" sum="906f276802fea718e3505c7953f0ff22" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter selection_sort.3.20" expl="for loop preservation" sum="37f0e9b766195456932095dc24ce6dd6" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
......
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