Commit 2325f49a authored by MARCHE Claude's avatar MARCHE Claude

simple examples and tests

parent 5d5daeba
theory CosineSingle
use import real.Real
use import real.Abs
use import real.Trigonometry
(* approximation of cosine function by 1 - x^2 / 2 on interval [-1/32; 1/32] *)
lemma MethodError: forall x:real. abs x <= 0x1p-5 ->
abs (1.0 - 0.5 * (x * x) - cos x) <= 0x1p-24
(* this one is proved in Coq + interval tactics *)
end
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Reals.Rbasic_fun.
Require Reals.R_sqrt.
Require Reals.Rtrigo_def.
Require Reals.Rtrigo1.
Require Reals.Ratan.
Require BuiltIn.
Require real.Real.
Require real.Abs.
Require real.Square.
Require real.Trigonometry.
(* Why3 goal *)
Theorem MethodError : forall (x:R),
((Reals.Rbasic_fun.Rabs x) <= (1 / 32)%R)%R ->
((Reals.Rbasic_fun.Rabs ((1%R - ((05 / 10)%R * (x * x)%R)%R)%R - (Reals.Rtrigo_def.cos x))%R) <= (1 / 16777216)%R)%R.
intros x h1.
Require Import Interval_tactic.
Qed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="MetiTarski" version="2.2" timelimit="5" memlimit="1000"/>
<prover id="1" name="Coq" version="8.4pl2" timelimit="5" memlimit="1000"/>
<file name="../real.why" expanded="true">
<theory name="CosineSingle" sum="9299bf587d5327dc3e513ff08d131a89" expanded="true">
<goal name="MethodError" sum="35ed1ba4221b1eb466cfdbfc5e895ef2" expanded="true">
<proof prover="0"><internalfailure reason="Printer.UnknownPrinter(&quot;metitarski&quot;)"/></proof>
<proof prover="1" edited="real_CosineSingle_MethodError_1.v" obsolete="true"><undone/></proof>
</goal>
</theory>
</file>
</why3session>
theory T
use import real.Real
use import real.MinMax
goal g: forall e p: real.
(2.0 * e + p + max e p) / 4.0 = max ((e+p)/2.0) ((3.0*e+p)/4.0)
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="CVC3"
version="2.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Z3"
version="2.19"/>
<prover
id="4"
name="Z3"
version="3.2"/>
<prover
id="5"
name="Z3"
version="4.0"/>
<file
name="../simple.why"
verified="true"
expanded="true">
<theory
name="T"
locfile="../simple.why"
loclnum="3" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="g"
locfile="../simple.why"
loclnum="8" loccnumb="7" loccnume="8"
sum="7925b3df5b9f5e28b19f5dbb26a89aba"
proved="true"
expanded="true"
shape="ainfix =ainfix /ainfix +ainfix +ainfix *c2.0V0V1amaxV0V1c4.0amaxainfix /ainfix +V0V1c2.0ainfix /ainfix +ainfix *c3.0V0V1c4.0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
/**************************************************************************/
/* */
/* The Why platform for program certification */
/* */
/* Copyright (C) 2002-2011 */
/* */
/* Jean-Christophe FILLIATRE, CNRS & Univ. Paris-sud 11 */
/* Claude MARCHE, INRIA & Univ. Paris-sud 11 */
/* Yannick MOY, Univ. Paris-sud 11 */
/* Romain BARDOU, Univ. Paris-sud 11 */
/* */
/* Secondary contributors: */
/* */
/* Thierry HUBERT, Univ. Paris-sud 11 (former Caduceus front-end) */
/* Nicolas ROUSSET, Univ. Paris-sud 11 (on Jessie & Krakatoa) */
/* Ali AYAD, CNRS & CEA Saclay (floating-point support) */
/* Sylvie BOLDO, INRIA (floating-point support) */
/* Jean-Francois COUCHOT, INRIA (sort encodings, hyps pruning) */
/* Mehdi DOGGUY, Univ. Paris-sud 11 (Why GUI) */
/* */
/* This software is free software; you can redistribute it and/or */
/* modify it under the terms of the GNU Lesser General Public */
/* License version 2.1, with the special exception on linking */
/* described in file LICENSE. */
/* */
/* This software is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. */
/* */
/**************************************************************************/
/*@ decreases 101-n ;
@ behavior less_than_101:
@ assumes n <= 100;
@ ensures \result == 91;
@ behavior greater_than_100:
@ assumes n >= 101;
@ ensures \result == n - 10;
@*/
int f91(int n) {
if (n <= 100) {
return f91(f91(n + 11));
}
else
return n - 10;
}
/*
Local Variables:
compile-command: "make rec.why3ide"
End:
*/
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) =
{ true }
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 (si, sf) = result in si = add_int l /\ sf = add_real l }
let main () =
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 module ref.Ref
exception Break
let sum (l: list or_integer_float) : (int, real) =
{ true }
let si = ref 0 in
let sf = ref 0.0 in
let ll = ref l in
try
while True do
invariant { !si + add_int !ll = add_int l /\
!sf +. add_real !ll = add_real l
}
match !ll with
| Nil -> raise Break
| Cons (Integer n) t ->
si := !si + n; ll := t
| Cons (Real x) t ->
sf := !sf +. x; ll := t
end
done;
absurd
with Break -> (!si, !sf)
end
{ let (si, sf) = result in si = add_int l /\ sf = add_real l }
let main () =
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
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
name="add_list/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.93"/>
<prover
id="1"
name="Alt-Ergo"
version="0.94"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<prover
id="3"
name="Z3"
version="3.2"/>
<file
name="../add_list.mlw"
verified="true"
expanded="true">
<theory
name="SumList"
locfile="add_list/../add_list.mlw"
loclnum="2" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
</theory>
<theory
name="WP AddListRec"
locfile="add_list/../add_list.mlw"
loclnum="28" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter sum"
locfile="add_list/../add_list.mlw"
loclnum="32" loccnumb="8" loccnume="11"
expl="parameter sum"
sum="864122fc1850685da889e50a016bf139"
proved="true"
expanded="true"
shape="CV0aNilainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aConsVVCV1aIntegerVainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aRealVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FF">
<label
name="expl:parameter sum"/>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter main"
locfile="add_list/../add_list.mlw"
loclnum="45" loccnumb="4" loccnume="8"
expl="parameter main"
sum="70fc66f484fe4f2dacec8be731a0e282"
proved="true"
expanded="true"
shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
<label
name="expl:parameter main"/>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
<theory
name="WP AddListImp"
locfile="add_list/../add_list.mlw"
loclnum="57" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter sum"
locfile="add_list/../add_list.mlw"
loclnum="64" loccnumb="4" loccnume="7"
expl="parameter sum"
sum="8c2e6fba3d93a8246e6ea9886fb15437"
proved="true"
expanded="true"
shape="CV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FFFAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
<label
name="expl:parameter sum"/>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter main"
locfile="add_list/../add_list.mlw"
loclnum="88" loccnumb="4" loccnume="8"
expl="parameter main"
sum="319b8c9fa71c762cd764adb846386504"
proved="true"
expanded="true"
shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
<label
name="expl:parameter main"/>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
module TestModule
(* module imports *)
use import int.Int
use import module ref.Ref
use import bool.Bool
use import list.List
use import list.Length
use import list.Nth
use import real.RealInfix
use import real.Abs
(* global variables declarations *)
val status : ref int
(* variables type declarations *)
type mm_integer = int
type mm_float = real
type or_integer_float = Integer mm_integer | Real mm_float
type list_or_integer_float = list or_integer_float
(* exceptions type declarations *)
type return_type = (int, real)
(* exceptions declarations *)
exception BreakLoop return_type
(* logical definitions of type tests *)
function type_test_or_integer_float_to_integer (x: or_integer_float) : bool =
match x with
| Integer mm_integer -> True
| Real mm_float -> False
end
function type_test_or_integer_float_to_float (x: or_integer_float) : bool =
match x with
| Integer mm_integer -> False
| Real mm_float -> True
end
(* auxiliary definitions and declarations *)
function get_nth (i: int) (l: list_or_integer_float) : or_integer_float =
match nth i l with
| None -> Real 0.0
| Some x -> x
end
axiom def_nth0: forall i: int, l: list_or_integer_float. 0 <= i < length(l) -> nth i l <> None
(*axiom def_length0: forall l: list_or_integer_float. length(l) > 0*)
(* logical type conversion functions *)
function or_integer_float_to_integer (e: or_integer_float) : mm_integer =
match e with
| Integer mm_integer -> mm_integer
| Real mm_float -> 1
end
function or_integer_float_to_float (e: or_integer_float) : mm_float =
match e with
| Integer mm_integer -> 1.0
| Real mm_float -> mm_float
end
(* logical auxiliary functions for specification *)
function add0 (e: list_or_integer_float) (i: int) (j: int) : mm_integer =
if i < j then
match e with
| Nil -> 0
| Cons h t -> if type_test_or_integer_float_to_integer (h) = True then
or_integer_float_to_integer (h) + add0 (t) (i+1) (j)
else
add0 (t) (i+1) (j)
end
else
0
function add1 (e: list_or_integer_float) (i: int) (j: int) : mm_float =
if i < j then
match e with
| Nil -> 0.0
| Cons h t -> if type_test_or_integer_float_to_float (h) = True then
or_integer_float_to_float (h) +. add1 (t)(i+1)(j)
else
add1 (t)(i+1)(j)
end
else
0.0
(* logical translation of procedure "sum (l: list(Or(integer, float)):[integer, float]" *)
let sum (l: list_or_integer_float) : (int, real) =
{true}
try
status := 0;
let si = ref 0 in
let sf = ref 0.0 in
let x = ref (any or_integer_float) in
for i = 0 to length(l)-1 do
invariant { !status >= 0 && (!si = add0(l)(0)(i) && !sf = add1(l)(0)(i) &&
(forall i0: int . 0 <= i0 < i -> ( type_test_or_integer_float_to_integer (get_nth i0 l) = True ->
or_integer_float_to_integer (get_nth i0 l) <> 0 ) )
&& (forall i0: int . 0 <= i0 < i -> ( type_test_or_integer_float_to_float (get_nth i0 l) = True ->
or_integer_float_to_float (get_nth i0 l) >=. 0.5 ) ) )}
status := i;
x := get_nth i l;
if type_test_or_integer_float_to_integer (!x) = True then
if or_integer_float_to_integer (!x) = 0 then
raise (BreakLoop (!si,!sf))
else
si := !si + or_integer_float_to_integer (!x)
else
if type_test_or_integer_float_to_float (!x) = True then
if or_integer_float_to_float (!x) <. 0.5 then
raise (BreakLoop (!si,!sf))
else
sf := !sf +. or_integer_float_to_float (!x)
done;
status := -1;
(!si,!sf)
with BreakLoop excp ->
match excp with
| (a0, a1) -> (a0, a1)
end
end
{
let (si0, sf0) = result in
( !status = -1
&& si0 = add0(l)(0)(length(l))
&& sf0 = add1(l)(0)(length(l))
&& (forall i0: int . 0 <= i0 < length(l) -> ( type_test_or_integer_float_to_integer (get_nth i0 l) = True ->
or_integer_float_to_integer (get_nth i0 l) <> 0 ) )
&& (forall i0: int . 0 <= i0 < length(l) -> ( type_test_or_integer_float_to_float (get_nth i0 l) = True ->
or_integer_float_to_float (get_nth i0 l) >=. 0.5 ) )
)
||
( 0 <= !status < length(l)
&& si0 = add0(l)(0)(!status)
&& sf0 = add1(l)(0)(!status)
&& ( (type_test_or_integer_float_to_integer (get_nth !status l) = True
&& or_integer_float_to_integer (get_nth !status l) = 0)
||
(type_test_or_integer_float_to_float (get_nth !status l) = True
&& or_integer_float_to_float (get_nth !status l) <. 0.5)
)
&& (forall i0: int . 0 <= i0 < !status -> ( type_test_or_integer_float_to_integer (get_nth i0 l) = True ->
or_integer_float_to_integer (get_nth i0 l) <> 0 ) )
&& (forall i0: int . 0 <= i0 < !status -> ( type_test_or_integer_float_to_float (get_nth i0 l) = True ->
or_integer_float_to_float (get_nth i0 l) >=. 0.5 ) )
)
}
let main () =
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 { !status = -1 };
assert { s = 22 };
assert { f = 4.7 }
end
This diff is collapsed.
module M
use import module ref.Ref
val x: ref int
let f () =
x := 1;
'L1:
x := 2;
'L2:
x := 3;
assert { (at !x 'L1) = 1 /\ (at !x 'L2) = 2 /\
(at (at !x 'L1) 'L2) = 1 /\
(at (at !x 'L2) 'L1) = 2 }
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="label/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
version="2.4.1"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="3.2"/>
<file
name="../label.mlw"
verified="false"
expanded="true">
<theory
name="WP M"
verified="false"
expanded="true">
<goal
name="WP_parameter f"
expl="assertion"
sum="ecb85905588ad84376c625fd8e5511e9"
proved="false"
expanded="true"
shape="ainfix =V0c2Aainfix =V0c1Aainfix =V1c2Aainfix =V0c1Iainfix =V2c3FIainfix =V1c2FIainfix =V0c1F">
<proof
prover="alt-ergo"
timelimit="3"
edited=""
obsolete="false">
<result status="unknown" time="0.04"/>