Commit 4d4181f9 authored by MARCHE Claude's avatar MARCHE Claude

updates a few more examples

parent 2a27363b
......@@ -11,7 +11,7 @@ suffix=$1
goods () {
pgm="bin/why3prove$suffix"
for f in $1/*.[wm][hl][yw] ; do
for f in $1/[e-z]*.[wm][hl][yw] ; do
echo -n " $f... "
# running Why
if ! $pgm $2 $f > /dev/null 2>&1; then
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
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 unit := unit.
Parameter fib: Z -> Z.
Axiom fib_def : forall (n:Z), (0%Z <= n)%Z -> (((n = 0%Z) ->
((fib n) = 0%Z)) /\ ((~ (n = 0%Z)) -> (((n = 1%Z) -> ((fib n) = 1%Z)) /\
((~ (n = 1%Z)) ->
((fib n) = ((fib (n - 1%Z)%Z) + (fib (n - 2%Z)%Z))%Z))))).
Axiom fib0 : ((fib 0%Z) = 0%Z).
Axiom fib1 : ((fib 1%Z) = 1%Z).
Axiom fibn : forall (n:Z), (2%Z <= n)%Z ->
((fib n) = ((fib (n - 1%Z)%Z) + (fib (n - 2%Z)%Z))%Z).
Axiom Abs_le : forall (x:Z) (y:Z), ((Zabs x) <= y)%Z <-> (((-y)%Z <= x)%Z /\
(x <= y)%Z).
Parameter div: Z -> Z -> Z.
Parameter mod1: Z -> Z -> Z.
Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x
y))%Z + (mod1 x y))%Z).
Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z).
(* Why3 assumption *)
Inductive t :=
| mk_t : Z -> Z -> Z -> Z -> t.
Axiom t_WhyType : WhyType t.
Existing Instance t_WhyType.
Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x
y))%Z /\ ((mod1 x y) < (Zabs y))%Z).
Axiom Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
Axiom Div_1 : forall (x:Z), ((div x 1%Z) = x).
Inductive t :=
| mk_t : Z -> Z -> Z -> Z -> t .
Definition a11(u:t): Z := match u with
| (mk_t a111 _ _ _) => a111
(* Why3 assumption *)
Definition a22 (v:t): Z := match v with
| (mk_t x x1 x2 x3) => x3
end.
Definition a12(u:t): Z := match u with
| (mk_t _ a121 _ _) => a121
(* Why3 assumption *)
Definition a21 (v:t): Z := match v with
| (mk_t x x1 x2 x3) => x2
end.
Definition a21(u:t): Z := match u with
| (mk_t _ _ a211 _) => a211
(* Why3 assumption *)
Definition a12 (v:t): Z := match v with
| (mk_t x x1 x2 x3) => x1
end.
Definition a22(u:t): Z := match u with
| (mk_t _ _ _ a221) => a221
(* Why3 assumption *)
Definition a11 (v:t): Z := match v with
| (mk_t x x1 x2 x3) => x
end.
Definition mult(x:t) (y:t): t :=
(* Why3 assumption *)
Definition mult (x:t) (y:t): t :=
(mk_t (((a11 x) * (a11 y))%Z + ((a12 x) * (a21 y))%Z)%Z
(((a11 x) * (a12 y))%Z + ((a12 x) * (a22 y))%Z)%Z
(((a21 x) * (a11 y))%Z + ((a22 x) * (a21 y))%Z)%Z
(((a21 x) * (a12 y))%Z + ((a22 x) * (a22 y))%Z)%Z).
Parameter power: t -> Z -> t.
Axiom Assoc : forall (x:t) (y:t) (z:t), ((mult (mult x y) z) = (mult x
(mult y z))).
Axiom Unit_def_l : forall (x:t), ((mult (mk_t 1%Z 0%Z 0%Z 1%Z) x) = x).
Axiom Unit_def_r : forall (x:t), ((mult x (mk_t 1%Z 0%Z 0%Z 1%Z)) = x).
Axiom Comm : forall (x:t) (y:t), ((mult x y) = (mult y x)).
Parameter power: t -> Z -> t.
Axiom Power_0 : forall (x:t), ((power x 0%Z) = (mk_t 1%Z 0%Z 0%Z 1%Z)).
Axiom Power_s : forall (x:t) (n:Z), (0%Z <= n)%Z -> ((power x
(n + 1%Z)%Z) = (mult x (power x n))).
Axiom Power_s_alt : forall (x:t) (n:Z), (0%Z < n)%Z -> ((power x n) = (mult x
(power x (n - 1%Z)%Z))).
Axiom Power_1 : forall (x:t), ((power x 1%Z) = x).
Axiom Power_sum : forall (x:t) (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) ->
((power x (n + m)%Z) = (mult (power x n) (power x m))).
Axiom Power_sum : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n + m)%Z) = (mult (power x n) (power x m)))).
Axiom Power_mult : forall (x:t) (n:Z) (m:Z), (0%Z <= n)%Z -> ((0%Z <= m)%Z ->
((power x (n * m)%Z) = (power (power x n) m))).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Hint Resolve fib0 fib1.
(* DO NOT EDIT BELOW *)
Axiom Power_mult2 : forall (x:t) (y:t) (n:Z), (0%Z <= n)%Z -> ((power (mult x
y) n) = (mult (power x n) (power y n))).
(* Why3 goal *)
Theorem fib_m : forall (n:Z), (0%Z <= n)%Z -> let p := (power (mk_t 1%Z 1%Z
1%Z 0%Z) n) in (((fib (n + 1%Z)%Z) = (a11 p)) /\ ((fib n) = (a21 p))).
(* Why3 intros n h1 p. *)
(* YOU MAY EDIT THE PROOF BELOW *)
intros n hn.
pattern n; apply natlike_ind; intuition.
......@@ -112,6 +103,4 @@ unfold a21, mult.
rewrite <- h1. rewrite <- h2.
unfold a21, a22. ring.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
......@@ -32,7 +32,7 @@ module Tarski_rec
let lemma least_fix_point () : unit
ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
= let rec aux (x: t) (b: set t) : t
= let rec ghost aux (x: t) (b: set t) : t
requires { mem x a /\ subset b a }
requires { forall y. mem y a -> rel x y -> mem y b }
requires { forall y. fixpoint y -> rel x y }
......@@ -64,4 +64,3 @@ module Tarski_while
done
end
......@@ -2,18 +2,50 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="1" memlimit="1000"/>
<file name="../finite_tarski.mlw" expanded="true">
<theory name="Tarski" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Tarski_rec" sum="1e15043844e2905232cb4e614e5f8246" expanded="true">
<goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
<proof prover="0"><result status="valid" time="0.15"/></proof>
<theory name="Tarski_rec" sum="0683581d76fb1f5c63aa43d29c8b9d42" expanded="true">
<goal name="VC least_fix_point" expl="VC for least_fix_point" expanded="true">
<proof prover="2"><result status="valid" time="0.10" steps="402"/></proof>
</goal>
</theory>
<theory name="Tarski_while" sum="dc3a928b725935c70c892f235fee1d02" expanded="true">
<goal name="WP_parameter least_fix_point" expl="VC for least_fix_point" expanded="true">
<proof prover="0"><result status="valid" time="0.19"/></proof>
<theory name="Tarski_while" sum="96f4bb3b979e6982e0bfdae3956e1abb" expanded="true">
<goal name="VC least_fix_point" expl="VC for least_fix_point" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC least_fix_point.1" expl="1. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC least_fix_point.2" expl="2. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC least_fix_point.3" expl="3. loop invariant init">
<proof prover="2"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="VC least_fix_point.4" expl="4. loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="VC least_fix_point.5" expl="5. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC least_fix_point.6" expl="6. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="54"/></proof>
</goal>
<goal name="VC least_fix_point.7" expl="7. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC least_fix_point.8" expl="8. loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC least_fix_point.9" expl="9. loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="64"/></proof>
</goal>
<goal name="VC least_fix_point.10" expl="10. postcondition">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
......
......@@ -12,32 +12,32 @@ module Flag
type color = Blue | White | Red
let eq_color (c1 c2 :color) : bool
ensures { result <-> c1 = c2 }
= match c1,c2 with
| Blue,Blue | Red,Red | White,White -> True
| _,_ -> False
end
predicate monochrome (a:map int color) (i:int) (j:int) (c:color) =
forall k:int. i <= k < j -> a[k]=c
function nb_occ (a:map int color) (i:int) (j:int) (c:color) : int
let rec function nb_occ (a:map int color) (i:int) (j:int) (c:color) : int
variant { j - i }
= if i >= j then 0 else
if eq_color a[j-1] c then 1 + nb_occ a i (j-1) c else nb_occ a i (j-1) c
axiom nb_occ_null:
forall a:map int color, i j:int, c:color.
i >= j -> nb_occ a i j c = 0
let rec lemma nb_occ_split (a:map int color) (i j k:int) (c:color)
requires { i <= j <= k }
variant { k - j }
ensures { nb_occ a i k c = nb_occ a i j c + nb_occ a j k c }
= if k = j then () else nb_occ_split a i j (k-1) c
axiom nb_occ_add_eq:
forall a:map int color, i j:int, c:color.
i < j /\ get a (j-1) = c -> nb_occ a i j c = nb_occ a i (j-1) c + 1
axiom nb_occ_add_neq:
forall a:map int color, i j:int, c:color.
i < j /\ get a (j-1) <> c -> nb_occ a i j c = nb_occ a i (j-1) c
lemma nb_occ_split:
forall a:map int color, i j k:int, c:color.
i <= j <= k ->
nb_occ a i k c = nb_occ a i j c + nb_occ a j k c
lemma nb_occ_ext:
forall a1 a2:map int color, i j:int, c:color.
(forall k:int. i <= k < j -> get a1 k = get a2 k) ->
nb_occ a1 i j c = nb_occ a2 i j c
let rec lemma nb_occ_ext (a1 a2:map int color) (i j:int) (c:color)
requires { forall k:int. i <= k < j -> a1[k] = a2[k] }
variant { j - i }
ensures { nb_occ a1 i j c = nb_occ a2 i j c }
= if i >= j then () else nb_occ_ext a1 a2 i (j-1) c
lemma nb_occ_store_outside_up:
forall a:map int color, i j k:int, c:color.
......@@ -49,56 +49,62 @@ module Flag
lemma nb_occ_store_eq_eq:
forall a:map int color, i j k:int, c:color.
i <= k < j -> get a k = c ->
i <= k < j -> a[k] = c ->
nb_occ (set a k c) i j c = nb_occ a i j c
lemma nb_occ_store_eq_neq:
forall a:map int color, i j k:int, c:color.
i <= k < j -> get a k <> c ->
nb_occ (set a k c) i j c = nb_occ a i j c + 1
let rec lemma nb_occ_store_eq_neq (a:map int color) (i j k:int) (c:color)
requires { i <= k < j }
requires { a[k] <> c }
variant { j - k }
ensures { nb_occ (set a k c) i j c = nb_occ a i j c + 1 }
= if k = j - 1 then () else nb_occ_store_eq_neq a i (j-1) k c
lemma nb_occ_store_neq_eq:
forall a:map int color, i j k:int, c c':color.
i <= k < j -> c <> c' -> get a k = c ->
i <= k < j -> c <> c' -> a[k] = c ->
nb_occ (set a k c') i j c = nb_occ a i j c - 1
lemma nb_occ_store_neq_neq:
forall a:map int color, i j k:int, c c':color.
i <= k < j -> c <> c' -> get a k <> c ->
i <= k < j -> c <> c' -> a[k] <> c ->
nb_occ (set a k c') i j c = nb_occ a i j c
use import array.Array
let swap (a:ref (map int color)) (i:int) (j:int) : unit
ensures { get !a i = get (old !a) j }
ensures { get !a j = get (old !a) i }
ensures { forall k:int. k <> i /\ k <> j -> get !a k = get (old !a) k }
let swap (a:array color) (i:int) (j:int) : unit
requires { 0 <= i < a.length }
requires { 0 <= j < a.length }
ensures { a[i] = old a[j] }
ensures { a[j] = old a[i] }
ensures { forall k:int. k <> i /\ k <> j -> a[k] = old a[k] }
ensures { forall k1 k2:int, c:color. k1 <= i < k2 /\ k1 <= j < k2 ->
nb_occ !a k1 k2 c = nb_occ (old !a) k1 k2 c }
= let ai = get !a i in
let aj = get !a j in
a := set !a i aj;
a := set !a j ai
nb_occ a.elts k1 k2 c = nb_occ (old a.elts) k1 k2 c }
= let ai = a[i] in
let aj = a[j] in
a[i] <- aj;
a[j] <- ai
let dutch_flag (a:ref (map int color)) (n:int)
requires { 0 <= n }
let dutch_flag (a:array color)
ensures { (exists b:int. exists r:int.
monochrome !a 0 b Blue /\
monochrome !a b r White /\
monochrome !a r n Red) }
ensures { forall c:color. nb_occ !a 0 n c = nb_occ (old !a) 0 n c }
monochrome a.elts 0 b Blue /\
monochrome a.elts b r White /\
monochrome a.elts r a.length Red) }
ensures { forall c:color.
nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
= let b = ref 0 in
let i = ref 0 in
let r = ref n in
let r = ref a.length in
while !i < !r do
invariant { 0 <= !b <= !i <= !r <= n }
invariant { monochrome !a 0 !b Blue }
invariant { monochrome !a !b !i White }
invariant { monochrome !a !r n Red }
invariant { 0 <= !b <= !i <= !r <= a.length }
invariant { monochrome a.elts 0 !b Blue }
invariant { monochrome a.elts !b !i White }
invariant { monochrome a.elts !r a.length Red }
invariant {
forall c:color. nb_occ !a 0 n c = nb_occ (old !a) 0 n c }
forall c:color.
nb_occ a.elts 0 a.length c = nb_occ (old a.elts) 0 a.length c }
variant { !r - !i }
match get !a !i with
match a[!i] with
| Blue -> swap a !b !i; b := !b + 1; i := !i + 1
| White -> i := !i + 1
| Red -> r := !r - 1; swap a !r !i
......
This diff is collapsed.
......@@ -701,6 +701,6 @@ end
(***
Local Variables:
compile-command: "why3ide sudoku.mlw"
compile-command: "why3 ide --extra-config ../share/strategies.conf sudoku.mlw"
End:
*)
This source diff could not be displayed because it is too large. You can view the blob instead.
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