Commit 40ae90d6 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

gcd example: renamed program functions to avoid confusion

parent 79831c22
......@@ -7,7 +7,7 @@ module EuclideanAlgorithm
use import number.Gcd
use import int.ComputerDivision
let rec gcd (u v: int) : int
let rec euclid (u v: int) : int
variant { v }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
......@@ -15,7 +15,7 @@ module EuclideanAlgorithm
if v = 0 then
u
else
gcd v (mod u v)
euclid v (mod u v)
end
......@@ -26,7 +26,7 @@ module EuclideanAlgorithmIterative
use import number.Gcd
use import int.ComputerDivision
let gcd (u0 v0: int) : int
let euclid (u0 v0: int) : int
requires { u0 >= 0 /\ v0 >= 0 }
ensures { result = gcd u0 v0 }
=
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
......@@ -12,28 +12,13 @@ Require number.Divisibility.
Require number.Gcd.
(* 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.
Definition unit := unit.
(* Why3 goal *)
Theorem WP_parameter_gcd : forall (u:Z), forall (v:Z), ((0%Z <= u)%Z /\
(0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> ((((0%Z <= v)%Z /\
((ZOmod u v) < v)%Z) /\ ((0%Z <= v)%Z /\ (0%Z <= (ZOmod u v))%Z)) ->
((number.Gcd.gcd v (ZOmod u v)) = (number.Gcd.gcd u v)))).
Theorem WP_parameter_euclid : forall (u:Z) (v:Z), ((0%Z <= u)%Z /\
(0%Z <= v)%Z) -> ((~ (v = 0%Z)) -> let o := (ZOmod u v) in
(((0%Z <= v)%Z /\ (0%Z <= o)%Z) -> ((number.Gcd.gcd v
o) = (number.Gcd.gcd u v)))).
Proof.
intuition.
symmetry.
......@@ -44,4 +29,3 @@ rewrite (ZO_div_mod_eq u v) at 1.
ring.
Qed.
......@@ -36,31 +36,31 @@
verified="true"
expanded="true">
<goal
name="WP_parameter gcd"
name="WP_parameter euclid"
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
expl="VC for gcd"
loclnum="10" loccnumb="10" loccnume="16"
expl="VC for euclid"
sum="b84585017fffbe0f504e8d89ce0def98"
proved="true"
expanded="true"
shape="iainfix =agcdV1V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V1c0Aainfix &lt;V2V1Aainfix &lt;=c0V1LamodV0V1ainfix =V0agcdV0V1ainfix =V1c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter gcd.1"
name="WP_parameter euclid.1"
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
loclnum="10" loccnumb="10" loccnume="16"
expl="1. postcondition"
sum="033ce819fc80e7096085ec758f6fe349"
proved="true"
expanded="true"
shape="postconditionainfix =V0agcdV0V1Iainfix =V1c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="2"
......@@ -87,16 +87,16 @@
</proof>
</goal>
<goal
name="WP_parameter gcd.2"
name="WP_parameter euclid.2"
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
loclnum="10" loccnumb="10" loccnume="16"
expl="2. variant decrease"
sum="f2ba394399ba521ce1cedb96dda922b6"
proved="true"
expanded="true"
shape="variant decreaseainfix &lt;V2V1Aainfix &lt;=c0V1LamodV0V1INainfix =V1c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="5"
......@@ -115,16 +115,16 @@
</proof>
</goal>
<goal
name="WP_parameter gcd.3"
name="WP_parameter euclid.3"
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
loclnum="10" loccnumb="10" loccnume="16"
expl="3. precondition"
sum="101f6236e5072dfb1a5699ed806a4717"
proved="true"
expanded="true"
shape="preconditionainfix &gt;=V2c0Aainfix &gt;=V1c0LamodV0V1INainfix =V1c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="10"
......@@ -151,16 +151,16 @@
</proof>
</goal>
<goal
name="WP_parameter gcd.4"
name="WP_parameter euclid.4"
locfile="../gcd.mlw"
loclnum="10" loccnumb="10" loccnume="13"
loclnum="10" loccnumb="10" loccnume="16"
expl="4. postcondition"
sum="1fc66eaeb9c88e73b45a64e02dc29d51"
proved="true"
expanded="true"
shape="postconditionainfix =agcdV1V2agcdV0V1Iainfix &gt;=V2c0Aainfix &gt;=V1c0LamodV0V1INainfix =V1c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="10"
......@@ -180,11 +180,11 @@
<proof
prover="3"
timelimit="10"
memlimit="0"
memlimit="1000"
edited="gcd_WP_EuclideanAlgorithm_WP_parameter_gcd_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.17"/>
<result status="valid" time="1.06"/>
</proof>
</goal>
</transf>
......@@ -197,31 +197,31 @@
verified="true"
expanded="true">
<goal
name="WP_parameter gcd"
name="WP_parameter euclid"
locfile="../gcd.mlw"
loclnum="29" loccnumb="6" loccnume="9"
expl="VC for gcd"
loclnum="29" loccnumb="6" loccnume="12"
expl="VC for euclid"
sum="d474f7a97f5c02e8730797c5e1cf11e4"
proved="true"
expanded="true"
shape="iainfix =V3agcdV0V1ainfix &lt;V4V2Aainfix &lt;=c0V2Aainfix =agcdV5V4agcdV0V1Aainfix &gt;=V4c0Aainfix &gt;=V5c0Iainfix =V5V2FIainfix =V4amodV3V2FNainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FAainfix &gt;=V1c0Aainfix &gt;=V0c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<transf
name="split_goal_wp"
proved="true"
expanded="true">
<goal
name="WP_parameter gcd.1"
name="WP_parameter euclid.1"
locfile="../gcd.mlw"
loclnum="29" loccnumb="6" loccnume="9"
loclnum="29" loccnumb="6" loccnume="12"
expl="1. loop invariant init"
sum="1366e7cebe0555bc0be81993c5836c21"
proved="true"
expanded="true"
shape="loop invariant initainfix &gt;=V1c0Aainfix &gt;=V0c0Iainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="10"
......@@ -232,16 +232,16 @@
</proof>
</goal>
<goal
name="WP_parameter gcd.2"
name="WP_parameter euclid.2"
locfile="../gcd.mlw"
loclnum="29" loccnumb="6" loccnume="9"
loclnum="29" loccnumb="6" loccnume="12"
expl="2. loop invariant preservation"
sum="9dcd65974a9bbc214b602b70371ae6e2"
proved="true"
expanded="true"
shape="loop invariant preservationainfix &gt;=V4c0Aainfix &gt;=V5c0Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="10"
......@@ -252,16 +252,16 @@
</proof>
</goal>
<goal
name="WP_parameter gcd.3"
name="WP_parameter euclid.3"
locfile="../gcd.mlw"
loclnum="29" loccnumb="6" loccnume="9"
loclnum="29" loccnumb="6" loccnume="12"
expl="3. loop invariant preservation"
sum="99474cb596c8b4cc5c787171b63b7146"
proved="true"
expanded="true"
shape="loop invariant preservationainfix =agcdV5V4agcdV0V1Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="10"
......@@ -272,16 +272,16 @@
</proof>
</goal>
<goal
name="WP_parameter gcd.4"
name="WP_parameter euclid.4"
locfile="../gcd.mlw"
loclnum="29" loccnumb="6" loccnume="9"
loclnum="29" loccnumb="6" loccnume="12"
expl="4. loop variant decrease"
sum="f8dd2ca54328343ceda03832078f78ca"
proved="true"
expanded="true"
shape="loop variant decreaseainfix &lt;V4V2Aainfix &lt;=c0V2Iainfix =V5V2FIainfix =V4amodV3V2FINainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="2"
timelimit="10"
......@@ -300,16 +300,16 @@
</proof>
</goal>
<goal
name="WP_parameter gcd.5"
name="WP_parameter euclid.5"
locfile="../gcd.mlw"
loclnum="29" loccnumb="6" loccnume="9"
loclnum="29" loccnumb="6" loccnume="12"
expl="5. postcondition"
sum="80e3f77c3f671a5e25f45b882719960c"
proved="true"
expanded="true"
shape="postconditionainfix =V3agcdV0V1INNainfix =V2c0Iainfix =agcdV3V2agcdV0V1Aainfix &gt;=V2c0Aainfix &gt;=V3c0FIainfix &gt;=V1c0Aainfix &gt;=V0c0F">
<label
name="expl:VC for gcd"/>
name="expl:VC for euclid"/>
<proof
prover="0"
timelimit="10"
......
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