Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

removed useless occurrences of int.Lex2

parent ee62233a
......@@ -5,7 +5,6 @@ module EWD673
use import bool.Bool
use import int.Int
use import int.Lex2
use import ref.Refint
val any_bool () : bool
......
......@@ -45,7 +45,6 @@ end
module BinaryGcd
use import mach.int.Int
use import int.Lex2
use import number.Parity
use import number.Gcd
......@@ -74,7 +73,7 @@ module BinaryGcd
odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v
let rec binary_gcd (u v: int) : int
variant { (v, u) with lex }
variant { v, u }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
=
......
......@@ -62,7 +62,7 @@
<goal name="VC binary_gcd" expl="VC for binary_gcd" proved="true">
<transf name="split_goal_right" proved="true" >
<goal name="VC binary_gcd.0" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC binary_gcd.1" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="7"/></proof>
......@@ -80,7 +80,7 @@
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.6" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC binary_gcd.7" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="18"/></proof>
......@@ -89,7 +89,7 @@
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="20"/></proof>
<proof prover="9"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="VC binary_gcd.10" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
......@@ -101,7 +101,7 @@
<proof prover="9"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.13" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="9"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="VC binary_gcd.14" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
......@@ -110,7 +110,7 @@
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.02" steps="24"/></proof>
<proof prover="9"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC binary_gcd.17" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
......
......@@ -45,7 +45,6 @@ end
module BinaryGcd
use import mach.int.Int
use import int.Lex2
use import number.Parity
use import number.Gcd
......@@ -74,7 +73,7 @@ module BinaryGcd
odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v
let rec binary_gcd (u v: int) : int
variant { (v, u) with lex }
variant { v, u }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
= [@vc:sp]
......
......@@ -2,6 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.7.1" timelimit="0" steplimit="0" memlimit="0"/>
......@@ -65,7 +66,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.6" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC binary_gcd.7" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -74,7 +75,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC binary_gcd.10" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -86,7 +87,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.13" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC binary_gcd.14" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
......@@ -95,7 +96,7 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC binary_gcd.17" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
......@@ -112,13 +113,13 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="VC binary_gcd.18.3" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.18.4" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.07"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.18.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
......
......@@ -28,7 +28,6 @@ module PrimeNumbers
use import int.Int
use import int.ComputerDivision
use import int.Lex2
use import number.Parity
use import number.Divisibility
use import number.Prime
......
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