Commit 3a3ac3b5 authored by MARCHE Claude's avatar MARCHE Claude

examples using vc:sp

parent 7dbc836a
theory SumList
use export int.Int
use export real.RealInfix
use export list.List
type or_integer_float = Integer int | Real real
(* sum integers in a list *)
function add_int (e: list or_integer_float) : int =
match e with
| Nil -> 0
| Cons (Integer n) t -> n + add_int t
| Cons _ t -> add_int t
end
(* sum reals in a list *)
function add_real (e: list or_integer_float) : real =
match e with
| Nil -> 0.0
| Cons (Real x) t -> x +. add_real t
| Cons _ t -> add_real t
end
end
module AddListRec
use import SumList
let rec sum (l: list or_integer_float) : (int, real) =
variant { l }
returns { si, sf -> si = add_int l /\ sf = add_real l }
"vc:sp"
match l with
| Nil -> 0, 0.0
| Cons h t ->
let a,b = sum t in
match h with
| Integer n -> n + a, b
| Real x -> a, x +. b
end
end
let main () =
"vc:sp"
let l =
Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
(Cons (Real 1.4) (Cons (Integer 9) Nil))))
in
let s,f = sum l in
assert { s = 22 };
assert { f = 4.7 }
end
module AddListImp
use import SumList
use import ref.Ref
let sum (l: list or_integer_float) : (int, real) =
returns { si, sf -> si = add_int l /\ sf = add_real l }
"vc:sp"
let si = ref 0 in
let sf = ref 0.0 in
let ll = ref l in
while True do
invariant { !si + add_int !ll = add_int l /\
!sf +. add_real !ll = add_real l }
variant { !ll }
match !ll with
| Nil -> return !si, !sf
| Cons (Integer n) t ->
si := !si + n; ll := t
| Cons (Real x) t ->
sf := !sf +. x; ll := t
end
done;
absurd
let main () =
"vc:sp"
let l =
Cons (Integer 5) (Cons (Real 3.3) (Cons (Integer 8)
(Cons (Real 1.4) (Cons (Integer 9) Nil))))
in
let s,f = sum l in
assert { s = 22 };
assert { f = 4.7 }
end
......@@ -2,24 +2,24 @@
<!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.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../add_list.mlw" expanded="true">
<theory name="SumList" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../add_list_vc_sp.mlw" proved="true">
<theory name="SumList" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="AddListRec" sum="191e311078f6223c9af44eece1bb2a47" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<theory name="AddListRec" proved="true" sum="191e311078f6223c9af44eece1bb2a47">
<goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<goal name="VC main" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="AddListImp" sum="25869898cb7ed98962558d9845b87089" expanded="true">
<goal name="VC sum" expl="VC for sum" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<theory name="AddListImp" proved="true" sum="8e8899af132298f23d25fda654d93382">
<goal name="VC sum" expl="VC for sum" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main" expl="VC for main" expanded="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<goal name="VC main" expl="VC for main" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
</file>
......
(* Binary search
A classical example. Searches a sorted array for a given value v. *)
module BinarySearch
use import int.Int
use import int.ComputerDivision
use import ref.Ref
use import array.Array
(* the code and its specification *)
exception Not_found (* raised to signal a search failure *)
let binary_search (a : array int) (v : int) : int
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
= "vc:sp"
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
invariant { 0 <= !l /\ !u < length a }
invariant {
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = !l + div (!u - !l) 2 in
assert { !l <= m <= !u };
if a[m] < v then
l := m + 1
else if a[m] > v then
u := m - 1
else
return m
done;
raise Not_found
end
(* A generalization: the midpoint is computed by some abstract function.
The only requirement is that it lies between l and u. *)
module BinarySearchAnyMidPoint
use import int.Int
use import ref.Ref
use import array.Array
exception Not_found (* raised to signal a search failure *)
val midpoint (l:int) (u:int) : int
requires { l <= u } ensures { l <= result <= u }
let binary_search (a :array int) (v : int) : int
requires { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
ensures { 0 <= result < length a /\ a[result] = v }
raises { Not_found -> forall i:int. 0 <= i < length a -> a[i] <> v }
= "vc:sp"
let l = ref 0 in
let u = ref (length a - 1) in
while !l <= !u do
invariant { 0 <= !l /\ !u < length a }
invariant {
forall i : int. 0 <= i < length a -> a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = midpoint !l !u in
if a[m] < v then
l := m + 1
else if a[m] > v then
u := m - 1
else
return m
done;
raise Not_found
end
(* binary search using 32-bit integers *)
module BinarySearchInt32
use import int.Int
use import mach.int.Int32
use import ref.Ref
use import mach.array.Array32
(* the code and its specification *)
exception Not_found (* raised to signal a search failure *)
let binary_search (a : array int32) (v : int32) : int32
requires { forall i1 i2 : int. 0 <= i1 <= i2 < to_int a.length ->
to_int a[i1] <= to_int a[i2] }
ensures { 0 <= to_int result < to_int a.length /\ a[to_int result] = v }
raises { Not_found ->
forall i:int. 0 <= i < to_int a.length -> a[i] <> v }
= "vc:sp"
let l = ref (of_int 0) in
let u = ref (length a - of_int 1) in
while !l <= !u do
invariant { 0 <= to_int !l /\ to_int !u < to_int a.length }
invariant { forall i : int. 0 <= i < to_int a.length ->
a[i] = v -> to_int !l <= i <= to_int !u }
variant { to_int !u - to_int !l }
let m = !l + (!u - !l) / of_int 2 in
assert { to_int !l <= to_int m <= to_int !u };
if a[m] < v then
l := m + of_int 1
else if a[m] > v then
u := m - of_int 1
else
return m
done;
raise Not_found
end
(* A particular case with Boolean values (0 or 1) and a sentinel 1 at the end.
We look for the first position containing a 1. *)
module BinarySearchBoolean
use import int.Int
use import int.ComputerDivision
use import ref.Ref
use import array.Array
let binary_search (a: array int) : int
requires { 0 < a.length }
requires { forall i j. 0 <= i <= j < a.length -> 0 <= a[i] <= a[j] <= 1 }
requires { a[a.length - 1] = 1 }
ensures { 0 <= result < a.length }
ensures { a[result] = 1 }
ensures { forall i. 0 <= i < result -> a[i] = 0 }
= "vc:sp"
let lo = ref 0 in
let hi = ref (length a - 1) in
while !lo < !hi do
invariant { 0 <= !lo <= !hi < a.length }
invariant { a[!hi] = 1 }
invariant { forall i. 0 <= i < !lo -> a[i] = 0 }
variant { !hi - !lo }
let mid = !lo + div (!hi - !lo) 2 in
if a[mid] = 1 then
hi := mid
else
lo := mid + 1
done;
!lo
end
......@@ -2,185 +2,26 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../binary_search.mlw" expanded="true">
<theory name="BinarySearch" sum="98ef67ab3183bf12850a4f30994ca1c1" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC binary_search.2" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC binary_search.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC binary_search.4" expl="assertion">
<proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC binary_search.5" expl="index in array bounds">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC binary_search.6" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC binary_search.7" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC binary_search.8" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="VC binary_search.9" expl="index in array bounds">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC binary_search.10" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC binary_search.11" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC binary_search.12" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="35"/></proof>
</goal>
<goal name="VC binary_search.13" expl="postcondition">
<proof prover="2"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_search.14" expl="exceptional postcondition">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</transf>
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../binary_search_vc_sp.mlw" proved="true">
<theory name="BinarySearch" proved="true" sum="9993e5984f553599fa3101436646fad3">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="BinarySearchAnyMidPoint" sum="8456c075486d647b4e64e1bc98b1f42a" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="VC binary_search.2" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC binary_search.3" expl="precondition">
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC binary_search.4" expl="index in array bounds">
<proof prover="2"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC binary_search.5" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC binary_search.6" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC binary_search.7" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="VC binary_search.8" expl="index in array bounds">
<proof prover="2"><result status="valid" time="0.00" steps="7"/></proof>
</goal>
<goal name="VC binary_search.9" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC binary_search.10" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC binary_search.11" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.00" steps="29"/></proof>
</goal>
<goal name="VC binary_search.12" expl="postcondition">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC binary_search.13" expl="exceptional postcondition">
<proof prover="2"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</transf>
<theory name="BinarySearchAnyMidPoint" proved="true" sum="3973fb0e710d4ec1c08923db54c5f93f">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" sum="066a83a4b67d1522f716af13c04d4224" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search">
<transf name="split_goal_wp">
<goal name="VC binary_search.1" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="VC binary_search.2" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.02" steps="72"/></proof>
</goal>
<goal name="VC binary_search.3" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.03" steps="79"/></proof>
</goal>
<goal name="VC binary_search.4" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="73"/></proof>
</goal>
<goal name="VC binary_search.5" expl="loop invariant init">
<proof prover="2"><result status="valid" time="0.02" steps="78"/></proof>
</goal>
<goal name="VC binary_search.6" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.03" steps="77"/></proof>
</goal>
<goal name="VC binary_search.7" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.07" steps="114"/></proof>
</goal>
<goal name="VC binary_search.8" expl="division by zero">
<proof prover="2"><result status="valid" time="0.02" steps="78"/></proof>
</goal>
<goal name="VC binary_search.9" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.11" steps="142"/></proof>
</goal>
<goal name="VC binary_search.10" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.16" steps="192"/></proof>
</goal>
<goal name="VC binary_search.11" expl="assertion">
<proof prover="2"><result status="valid" time="0.12" steps="161"/></proof>
</goal>
<goal name="VC binary_search.12" expl="index in array bounds">
<proof prover="2"><result status="valid" time="0.02" steps="82"/></proof>
</goal>
<goal name="VC binary_search.13" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.02" steps="84"/></proof>
</goal>
<goal name="VC binary_search.14" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.20" steps="177"/></proof>
</goal>
<goal name="VC binary_search.15" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="VC binary_search.16" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="86"/></proof>
</goal>
<goal name="VC binary_search.17" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.18" steps="200"/></proof>
</goal>
<goal name="VC binary_search.18" expl="index in array bounds">
<proof prover="2"><result status="valid" time="0.03" steps="83"/></proof>
</goal>
<goal name="VC binary_search.19" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.02" steps="85"/></proof>
</goal>
<goal name="VC binary_search.20" expl="integer overflow">
<proof prover="2"><result status="valid" time="0.41" steps="180"/></proof>
</goal>
<goal name="VC binary_search.21" expl="loop variant decrease">
<proof prover="2"><result status="valid" time="0.02" steps="87"/></proof>
</goal>
<goal name="VC binary_search.22" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.03" steps="87"/></proof>
</goal>
<goal name="VC binary_search.23" expl="loop invariant preservation">
<proof prover="2"><result status="valid" time="0.15" steps="201"/></proof>
</goal>
<goal name="VC binary_search.24" expl="postcondition">
<proof prover="2"><result status="valid" time="0.07" steps="141"/></proof>
</goal>
<goal name="VC binary_search.25" expl="exceptional postcondition">
<proof prover="2"><result status="valid" time="0.03" steps="80"/></proof>
</goal>
</transf>
<theory name="BinarySearchInt32" proved="true" sum="ee5d1d580f7e99f5096f0d4896d70261">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
</theory>
<theory name="BinarySearchBoolean" sum="0022604a394766cd083f25712d0f873a" expanded="true">
<goal name="VC binary_search" expl="VC for binary_search" expanded="true">
<proof prover="2"><result status="valid" time="0.09" steps="194"/></proof>
<theory name="BinarySearchBoolean" proved="true" sum="0022604a394766cd083f25712d0f873a">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
</theory>
</file>
......
(* Various programs computing the factorial. *)
module FactRecursive
use import int.Int
use import int.Fact
let rec fact_rec (x:int) : int
requires { x >= 0 }
variant { x }
ensures { result = fact x }
= "vc:sp"
if x = 0 then 1 else x * fact_rec (x-1)
let test0 () = fact_rec 0
let test1 () = fact_rec 1
let test7 () = fact_rec 7
let test42 () = fact_rec 42
end
module FactImperative
use import int.Int
use import int.Fact
use import ref.Ref
let fact_imp (x:int) : int
requires { x >= 0 }
ensures { result = fact x }
= "vc:sp"
let y = ref 0 in
let r = ref 1 in
while !y < x do
invariant { 0 <= !y <= x }
invariant { !r = fact !y }
variant { x - !y }
y := !y + 1;
r := !r * !y
done;
!r
let test0 () = fact_imp 0
let test1 () = fact_imp 1
let test7 () = fact_imp 7
let test42 () = fact_imp 42
end
......@@ -2,40 +2,40 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../fact.mlw" expanded="true">
<theory name="FactRecursive" sum="919362d8ebfa7553f31188fdb9ff9151" expanded="true">
<goal name="VC fact_rec" expl="VC for fact_rec" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="16"/></proof>
<prover id="0" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../fact_vc_sp.mlw" proved="true">
<theory name="FactRecursive" proved="true" sum="919362d8ebfa7553f31188fdb9ff9151">
<goal name="VC fact_rec" expl="VC for fact_rec" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC test0" expl="VC for test0" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
<goal name="VC test0" expl="VC for test0" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC test1" expl="VC for test1" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
<goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC test7" expl="VC for test7" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="0"/></proof>
<goal name="VC test7" expl="VC for test7" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC test42" expl="VC for test42" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
<goal name="VC test42" expl="VC for test42" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="FactImperative" sum="f774c4a73a685d4f4ee9f137ea770ccf" expanded="true">
<goal name="VC fact_imp" expl="VC for fact_imp" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="23"/></proof>
<theory name="FactImperative" proved="true" sum="f774c4a73a685d4f4ee9f137ea770ccf">
<goal name="VC fact_imp" expl="VC for fact_imp" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC test0" expl="VC for test0" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
<goal name="VC test0" expl="VC for test0" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC test1" expl="VC for test1" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<goal name="VC test1" expl="VC for test1" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC test7" expl="VC for test7" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
<goal name="VC test7" expl="VC for test7" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC test42" expl="VC for test42" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
<goal name="VC test42" expl="VC for test42" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
</file>
......
......@@ -12,13 +12,6 @@ Require number.Gcd.
Require number.Prime.
Require number.Coprime.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
......
(** {1 Greatest common divisor, with Bézout coefficients} *)
module GcdBezout
use import int.Int
use import int.ComputerDivision
use import number.Gcd
use import ref.Ref
let gcd (x:int) (y:int)
requires { x >= 0 /\ y >= 0 }
ensures { result = gcd x y }
ensures { exists a b:int. a*x+b*y = result }
= "vc:sp"
let x = ref x in let y = ref y in
label Pre in
let ghost a = ref 1 in let ghost b = ref 0 in
let ghost c = ref 0 in let ghost d = ref 1 in
while (!y > 0) do
invariant { !x >= 0 /\ !y >= 0 }
invariant { gcd !x !y = gcd (!x at Pre) (!y at Pre) }
invariant { !a * (!x at Pre) + !b * (!y at Pre) = !x }
invariant { !c * (!x at Pre) + !d * (!y at Pre) = !y }
variant { !y }
let r = mod !x !y in let ghost q = div !x !y in
assert { r = !x - q * !y };
x := !y; y := r;
let ghost ta = !a in let ghost tb = !b in
a := !c; b := !d;
c := ta - !c * q; d := tb - !d * q;
done;
!x
end
......@@ -2,54 +2,53 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../gcd_bezout.mlw" expanded="true">
<theory name="GcdBezout" sum="6d4ff8bdfabfccd6c9451c7f2fc39247" expanded="true">
<goal name="VC gcd" expl="VC for gcd" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC gcd.1" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../gcd_bezout_vc_sp.mlw" proved="true">
<theory name="GcdBezout" proved="true" sum="d9cc50540312b9e45a005a2e3d6f7128">
<goal name="VC gcd" expl="VC for gcd" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC gcd.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.2" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
<goal name="VC gcd.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.3" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="2"/></proof>
<goal name="VC gcd.2" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.4" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
<goal name="VC gcd.3" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.5" expl="precondition">
<proof prover="0"><result status="valid" time="0.03" steps="8"/></proof>
<goal name="VC gcd.4" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.6" expl="precondition">
<proof prover="0"><result status="valid" time="0.02" steps="8"/></proof>
<goal name="VC gcd.5" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC gcd.7" expl="assertion">
<proof prover="0"><result status="valid" time="0.03" steps="12"/></proof>
<goal name="VC gcd.6" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC gcd.8" expl="loop variant decrease">