Commit ba40786e authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Merge branch 'master' into mp (alias, range types machine integers)

Conflicts:
	modules/mach/int.mlw
	plugins/python/py_parser.mly
	src/mlw/dexpr.ml
	src/parser/parser.mly
parents 85e816e8 26335a9a
......@@ -210,8 +210,8 @@ module mach.int.Int63
syntax literal int63 "%1"
syntax converter of_int "%1"
syntax val of_int "Z.to_int %1"
syntax function to_int "Z.of_int %1"
syntax val of_int "Z.to_int %1"
syntax val to_int "Z.of_int %1"
syntax constant min_int63 "Z.of_int min_int"
syntax constant max_int63 "Z.of_int max_int"
......@@ -323,9 +323,9 @@ end
module mach.int.Refint63
syntax val incr "incr %1"
syntax val decr "decr %1"
syntax val (+=) "%1 := !%1 + %2" (*"(fun r v -> Pervasives.(:=) r (Pervasives.(!) r + v))"*)
syntax val (-=) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r - v))"
syntax val ( *= ) "(fun r v -> Pervasives.(:=) r (Pervasives.(!) r * v))"
syntax val (+=) "%1 := !%1 + %2"
syntax val (-=) "%1 := !%1 - %2"
syntax val ( *= ) "%1 := !%1 * %2"
end
module mach.int.MinMax63
syntax val min "Pervasives.min %1 %2"
......
......@@ -90,25 +90,25 @@ module BinarySearchInt32
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 }
requires { forall i1 i2 : int. 0 <= i1 <= i2 < a.length ->
a[i1] <= a[i2] }
ensures { 0 <= result < a.length /\ a[result] = v }
raises { Not_found ->
forall i:int. 0 <= i < to_int a.length -> a[i] <> v }
forall i:int. 0 <= i < a.length -> a[i] <> v }
=
let l = ref (of_int 0) in
let u = ref (length a - of_int 1) in
let l = ref 0 in
let u = ref (length a - 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 };
invariant { 0 <= !l /\ !u < a.length }
invariant { forall i : int. 0 <= i < a.length ->
a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = !l + (!u - !l) / 2 in
assert { !l <= m <= !u };
if a[m] < v then
l := m + of_int 1
l := m + 1
else if a[m] > v then
u := m - of_int 1
u := m - 1
else
return m
done;
......
......@@ -14,9 +14,9 @@
<proof prover="3"><result status="valid" time="0.01" steps="63"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true" sum="909f26be7787adc1464e7f847a908692">
<theory name="BinarySearchInt32" proved="true" sum="189de117608870d3dac4a21f7234eef5">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="3"><result status="valid" time="2.53" steps="3682"/></proof>
<proof prover="3"><result status="valid" time="8.18" steps="11481"/></proof>
</goal>
</theory>
<theory name="BinarySearchBoolean" proved="true" sum="0022604a394766cd083f25712d0f873a">
......
......@@ -90,25 +90,25 @@ module BinarySearchInt32
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 }
requires { forall i1 i2 : int. 0 <= i1 <= i2 < a.length ->
a[i1] <= a[i2] }
ensures { 0 <= result < a.length /\ a[result] = v }
raises { Not_found ->
forall i:int. 0 <= i < to_int a.length -> a[i] <> v }
forall i:int. 0 <= i < a.length -> a[i] <> v }
= "vc:sp"
let l = ref (of_int 0) in
let u = ref (length a - of_int 1) in
let l = ref 0 in
let u = ref (length a - 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 };
invariant { 0 <= !l /\ !u < a.length }
invariant { forall i : int. 0 <= i < a.length ->
a[i] = v -> !l <= i <= !u }
variant { !u - !l }
let m = !l + (!u - !l) / 2 in
assert { !l <= m <= !u };
if a[m] < v then
l := m + of_int 1
l := m + 1
else if a[m] > v then
u := m - of_int 1
u := m - 1
else
return m
done;
......
......@@ -14,7 +14,7 @@
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</theory>
<theory name="BinarySearchInt32" proved="true" sum="c9f0cf881df8be787d964ba3de51306f">
<theory name="BinarySearchInt32" proved="true" sum="0aeaeda1d3225a20418f2d07e713896a">
<goal name="VC binary_search" expl="VC for binary_search" proved="true">
<proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
......
......@@ -101,10 +101,10 @@ module EuclideanAlgorithm31
let rec euclid (u v: int31) : int31
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
=
if Int31.eq v (of_int 0) then
if v = 0 then
u
else
euclid v (u % v)
......@@ -119,10 +119,10 @@ module EuclideanAlgorithm63
let rec euclid (u v: int63) : int63
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
=
if v = of_int 0 then
if v = 0 then
u
else
euclid v (u % v)
......
......@@ -7,132 +7,132 @@
<prover id="3" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../gcd.mlw" expanded="true">
<theory name="EuclideanAlgorithm" sum="7aa7887c1d4eda9747b55d845d4f7a9e" expanded="true">
<goal name="VC euclid" expl="VC for euclid">
<transf name="split_goal_wp">
<goal name="VC euclid.1" expl="check modulo by zero">
<file name="../gcd.mlw" proved="true">
<theory name="EuclideanAlgorithm" proved="true" sum="44d7bb87668a49a2f2a4f5b307eac883">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC euclid.0" expl="check modulo by zero" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC euclid.2" expl="variant decrease">
<goal name="VC euclid.1" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="VC euclid.3" expl="precondition">
<goal name="VC euclid.2" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC euclid.4" expl="postcondition">
<goal name="VC euclid.3" expl="postcondition" proved="true">
<proof prover="9"><result status="valid" time="0.03" steps="47"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithmIterative" sum="3ff6d7d9dd6e825392762f38be2bf072" expanded="true">
<goal name="VC euclid" expl="VC for euclid">
<theory name="EuclideanAlgorithmIterative" proved="true" sum="3ff6d7d9dd6e825392762f38be2bf072">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="BinaryGcd" sum="2492b58eb155597878f9d226ab7b345b" expanded="true">
<goal name="even1" expl="">
<theory name="BinaryGcd" proved="true" sum="f288abe81fe0bb1c65550b0d7201e3b9">
<goal name="even1" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="odd1" expl="">
<goal name="odd1" proved="true">
<proof prover="9"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="div_nonneg" expl="">
<goal name="div_nonneg" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="gcd_even_even" expl="">
<goal name="gcd_even_even" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="gcd_even_odd" expl="">
<goal name="gcd_even_odd" proved="true">
<proof prover="3" edited="gcd_BinaryGcd_gcd_even_odd_2.v"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="gcd_even_odd2" expl="">
<goal name="gcd_even_odd2" proved="true">
<proof prover="9"><result status="valid" time="0.05" steps="29"/></proof>
</goal>
<goal name="odd_odd_div2" expl="">
<goal name="odd_odd_div2" proved="true">
<proof prover="9"><result status="valid" time="0.63" steps="389"/></proof>
</goal>
<goal name="VC gcd_odd_odd" expl="VC for gcd_odd_odd">
<goal name="VC gcd_odd_odd" expl="VC for gcd_odd_odd" proved="true">
<proof prover="9"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="gcd_odd_odd2" expl="">
<goal name="gcd_odd_odd2" proved="true">
<proof prover="9"><result status="valid" time="0.07" steps="30"/></proof>
</goal>
<goal name="VC binary_gcd" expl="VC for binary_gcd">
<transf name="split_goal_wp">
<goal name="VC binary_gcd.1" expl="variant decrease">
<goal name="VC binary_gcd" expl="VC for binary_gcd" proved="true">
<transf name="split_goal_wp" 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>
</goal>
<goal name="VC binary_gcd.2" expl="precondition">
<goal name="VC binary_gcd.1" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="VC binary_gcd.3" expl="precondition">
<goal name="VC binary_gcd.2" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.4" expl="precondition">
<goal name="VC binary_gcd.3" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC binary_gcd.5" expl="check division by zero">
<goal name="VC binary_gcd.4" expl="check division by zero" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.6" expl="check division by zero">
<goal name="VC binary_gcd.5" expl="check division by zero" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.7" expl="variant decrease">
<goal name="VC binary_gcd.6" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="VC binary_gcd.8" expl="precondition">
<goal name="VC binary_gcd.7" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC binary_gcd.9" expl="check division by zero">
<goal name="VC binary_gcd.8" expl="check division by zero" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.10" expl="variant decrease">
<goal name="VC binary_gcd.9" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="VC binary_gcd.11" expl="precondition">
<goal name="VC binary_gcd.10" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC binary_gcd.12" expl="precondition">
<goal name="VC binary_gcd.11" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.00" steps="9"/></proof>
</goal>
<goal name="VC binary_gcd.13" expl="check division by zero">
<goal name="VC binary_gcd.12" expl="check division by zero" proved="true">
<proof prover="9"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.14" expl="variant decrease">
<goal name="VC binary_gcd.13" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC binary_gcd.15" expl="precondition">
<goal name="VC binary_gcd.14" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC binary_gcd.16" expl="check division by zero">
<goal name="VC binary_gcd.15" expl="check division by zero" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC binary_gcd.17" expl="variant decrease">
<goal name="VC binary_gcd.16" expl="variant decrease" proved="true">
<proof prover="9"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="VC binary_gcd.18" expl="precondition">
<goal name="VC binary_gcd.17" expl="precondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="VC binary_gcd.19" expl="postcondition">
<transf name="split_goal_wp">
<goal name="VC binary_gcd.19.1" expl="postcondition">
<goal name="VC binary_gcd.18" expl="postcondition" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC binary_gcd.18.0" expl="postcondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="VC binary_gcd.19.2" expl="postcondition">
<goal name="VC binary_gcd.18.1" expl="postcondition" proved="true">
<proof prover="9"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC binary_gcd.19.3" expl="postcondition">
<goal name="VC binary_gcd.18.2" expl="postcondition" proved="true">
<proof prover="9"><result status="valid" time="0.12" steps="89"/></proof>
</goal>
<goal name="VC binary_gcd.19.4" expl="postcondition">
<goal name="VC binary_gcd.18.3" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC binary_gcd.19.5" expl="postcondition">
<goal name="VC binary_gcd.18.4" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC binary_gcd.19.6" expl="postcondition">
<goal name="VC binary_gcd.18.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
......@@ -140,8 +140,8 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm63" sum="b8b13e83f3d237bbc360c6f9f88ef153" expanded="true">
<goal name="VC euclid" expl="VC for euclid">
<theory name="EuclideanAlgorithm63" proved="true" sum="2957f2c27fa5f1ab089e561053c1d9ac">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="1"><result status="valid" time="0.24"/></proof>
</goal>
</theory>
......
......@@ -101,10 +101,10 @@ module EuclideanAlgorithm31
let rec euclid (u v: int31) : int31
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
=
if Int31.eq v (of_int 0) then
if v = 0 then
u
else
euclid v (u % v)
......@@ -119,10 +119,10 @@ module EuclideanAlgorithm63
let rec euclid (u v: int63) : int63
variant { to_int v }
requires { to_int u >= 0 /\ to_int v >= 0 }
ensures { to_int result = gcd (to_int u) (to_int v) }
requires { u >= 0 /\ v >= 0 }
ensures { result = gcd u v }
= "vc:sp"
if v = of_int 0 then
if v = 0 then
u
else
euclid v (u % v)
......
......@@ -125,7 +125,7 @@
</transf>
</goal>
</theory>
<theory name="EuclideanAlgorithm63" proved="true" sum="b8b13e83f3d237bbc360c6f9f88ef153">
<theory name="EuclideanAlgorithm63" proved="true" sum="2957f2c27fa5f1ab089e561053c1d9ac">
<goal name="VC euclid" expl="VC for euclid" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
......
......@@ -85,10 +85,10 @@ module McCarthy91Mach
let rec f91 (n: int63) : int63
variant { 101 - n }
ensures { result = spec n }
= if n <= of_int 100 then
f91 (f91 (n + of_int 11))
= if n <= 100 then
f91 (f91 (n + 11))
else
n - of_int 10
n - 10
use import mach.peano.Peano
use import mach.int.Refint63
......@@ -101,11 +101,11 @@ module McCarthy91Mach
while gt !e zero do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
variant { 101 - !n + 10 * !e, !e:int }
if !n > Int63.of_int 100 then begin
n := !n - Int63.of_int 10;
if !n > 100 then begin
n := !n - 10;
e := pred !e
end else begin
n := !n + Int63.of_int 11;
n := !n + 11;
e := succ !e
end
done;
......@@ -124,11 +124,11 @@ module McCarthy91Mach
else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
= if not (gt !e zero) then raise Stop;
if !n > Int63.of_int 100 then begin
n := !n - Int63.of_int 10;
if !n > 100 then begin
n := !n - 10;
e := pred !e
end else begin
n := !n + Int63.of_int 11;
n := !n + 11;
e := succ !e
end
in
......@@ -137,8 +137,8 @@ module McCarthy91Mach
variant { 101 - !n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
raises { Stop -> false }
= let u = !n in bloc (); if u <= Int63.of_int 100 then (aux (); aux ()) in
= let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd
with Stop -> !n end
end
\ No newline at end of file
end
......@@ -3,27 +3,27 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../mccarthy.mlw">
<theory name="McCarthy91" sum="13b896e51d6f77e4be03ed7c66d03ca8">
<goal name="VC f91" expl="VC for f91">
<file name="../mccarthy.mlw" proved="true">
<theory name="McCarthy91" proved="true" sum="13b896e51d6f77e4be03ed7c66d03ca8">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.00" steps="31"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec">
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.29" steps="517"/></proof>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec">
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="0.01" steps="49"/></proof>
</goal>
</theory>
<theory name="McCarthy91Mach" sum="b37d5db478b81235db7385d87cd66422">
<goal name="VC f91" expl="VC for f91">
<proof prover="1"><result status="valid" time="0.07" steps="336"/></proof>
<theory name="McCarthy91Mach" proved="true" sum="7d4600e0ee1b08517405296863b5c9d8">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.07" steps="1067"/></proof>
</goal>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec">
<proof prover="1"><result status="valid" time="4.23" steps="10650"/></proof>
<goal name="VC f91_nonrec" expl="VC for f91_nonrec" proved="true">
<proof prover="1"><result status="valid" time="6.06" steps="12891"/></proof>
</goal>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec">
<proof prover="1"><result status="valid" time="0.26" steps="925"/></proof>
<goal name="VC f91_pseudorec" expl="VC for f91_pseudorec" proved="true">
<proof prover="1"><result status="valid" time="0.08" steps="432"/></proof>
</goal>
</theory>
</file>
......
......@@ -85,10 +85,10 @@ module McCarthy91Mach
let rec f91 (n: int63) : int63
variant { 101 - n }
ensures { result = spec n }
= "vc:sp" if n <= of_int 100 then
f91 (f91 (n + of_int 11))
= "vc:sp" if n <= 100 then
f91 (f91 (n + 11))
else
n - of_int 10
n - 10
use import mach.peano.Peano
use import mach.int.Refint63
......@@ -101,11 +101,11 @@ module McCarthy91Mach
while gt !e zero do
invariant { !e >= 0 /\ iter spec !e !n = spec n0 }
variant { 101 - !n + 10 * !e, !e:int }
if !n > Int63.of_int 100 then begin
n := !n - Int63.of_int 10;
if !n > 100 then begin
n := !n - 10;
e := pred !e
end else begin
n := !n + Int63.of_int 11;
n := !n + 11;
e := succ !e
end
done;
......@@ -124,11 +124,11 @@ module McCarthy91Mach
else !n = !(old n) + 11 /\ !e = !(old e) + 1 }
raises { Stop -> !e = !(old e) = 0 /\ !n = !(old n) }
= if not (gt !e zero) then raise Stop;
if !n > Int63.of_int 100 then begin
n := !n - Int63.of_int 10;
if !n > 100 then begin
n := !n - 10;
e := pred !e
end else begin
n := !n + Int63.of_int 11;
n := !n + 11;
e := succ !e
end
in
......@@ -137,8 +137,8 @@ module McCarthy91Mach
variant { 101 - !n }
ensures { !e = !(old e) - 1 /\ !n = spec !(old n) }
raises { Stop -> false }
= let u = !n in bloc (); if u <= Int63.of_int 100 then (aux (); aux ()) in
= let u = !n in bloc (); if u <= 100 then (aux (); aux ()) in
try aux (); bloc (); absurd
with Stop -> !n end
end
\ No newline at end of file
end
......@@ -16,7 +16,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="McCarthy91Mach" proved="true" sum="b37d5db478b81235db7385d87cd66422">
<theory name="McCarthy91Mach" proved="true" sum="7d4600e0ee1b08517405296863b5c9d8">
<goal name="VC f91" expl="VC for f91" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
......
......@@ -26,34 +26,31 @@ module SwapInt32
(* a simple model of 32-bit integers with addition, subtraction,
and possible overflows *)
type int32
type int32 = < range -0x8000_0000 0x7fff_ffff >
constant min_int32 : int = - 0x80000000
constant max_int32 : int = 0x7fffffff
constant width : int = max_int32 - min_int32 + 1
meta coercion function int32'int
function to_int (n: int32) : int
constant width : int = int32'maxInt - int32'minInt + 1
val (+) (a: int32) (b: int32) : int32
ensures { to_int result =
if to_int a + to_int b < min_int32 then to_int a + to_int b + width
else if to_int a + to_int b > max_int32 then to_int a + to_int b - width
else to_int a + to_int b }
ensures { result =
if a + b < int32'minInt then a + b + width
else if a + b > int32'maxInt then a + b - width
else a + b }
val (-) (a: int32) (b: int32) : int32
ensures { to_int result =
if to_int a - to_int b < min_int32 then to_int a - to_int b + width
else if to_int a - to_int b > max_int32 then to_int a - to_int b - width
else to_int a - to_int b }
ensures { result =
if a - b < int32'minInt then a - b + width
else if a - b > int32'maxInt then a - b - width
else a - b }
predicate in_bounds (n: int32) = min_int32 <= to_int n <= max_int32
predicate in_bounds (n: int32) = int32'minInt <= n <= int32'maxInt
(* purely applicative version first *)
let swap (a b: int32) : (int32, int32)
requires { in_bounds a /\ in_bounds b }
returns { x,y ->
to_int x = to_int b /\ to_int y = to_int a }
returns { x,y -> int32'int x = b /\ int32'int y = a }
=
let a = a + b in
let b = a - b in
......@@ -65,7 +62,7 @@ module SwapInt32
let swap_ref (a b: ref int32) : unit
requires { in_bounds !a /\ in_bounds !b }
writes { a, b }
ensures { to_int !a = old (to_int !b) /\ to_int !b = old (to_int !a) }
ensures { int32'int !a = old !b /\ int32'int !b = old !a }
=
a := !a + !b;
b := !a - !b;
......