Commit 7d674cf5 authored by MARCHE Claude's avatar MARCHE Claude

examples from BTS

parent 1267c59a
(*
BTS 13515
https://gforge.inria.fr/tracker/index.php?func=detail&aid=13515&group_id=2990
*)
module ExcepAndRec
use import int.Int
exception E
let rec f (x:int) : int =
if x = 42 then raise E else
try
let n = f (x-1) in
n
with E -> 42
end
end
(*
BTS 13853
https://gforge.inria.fr/tracker/?func=detail&atid=10293&aid=13853&group_id=2990
*)
module T
use import int.Int
exception MyExc
let rec f (x:int) : int = {} raise MyExc {} | MyExc -> {}
with g (x:int) : int = {} f x {} | MyExc -> {}
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="13853/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<file
name="../13853.mlw"
verified="true"
expanded="true">
<theory
name="WP T"
locfile="13853/../13853.mlw"
loclnum="10" loccnumb="7" loccnume="8"
verified="true"
expanded="true">
<goal
name="WP_parameter f"
locfile="13853/../13853.mlw"
loclnum="16" loccnumb="8" loccnume="9"
expl="exceptional postcondition"
sum="ae08fd30941b510f8d344e85ce6d2985"
proved="true"
expanded="false"
shape="t">
<label
name="expl:parameter f">
</label>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter g"
locfile="13853/../13853.mlw"
loclnum="18" loccnumb="7" loccnume="8"
expl="exceptional postcondition"
sum="4a3609e7c6245ef3b76fa886e82409e2"
proved="true"
expanded="false"
shape="t">
<label
name="expl:parameter g">
</label>
<proof
prover="0"
timelimit="10"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</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