Commit 979c40e7 authored by MARCHE Claude's avatar MARCHE Claude

new small program example, inspired by Taimoor Khan

parent aee6644c
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.94"/>
<prover
id="1"
name="CVC3"
version="2.4.1"/>
<prover
id="2"
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="29" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter sum"
locfile="add_list/../add_list.mlw"
loclnum="33" 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="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="2"
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="46" 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="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
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="58" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter sum"
locfile="add_list/../add_list.mlw"
loclnum="65" 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="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
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="89" 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="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</theory>
</file>
</why3session>
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