Commit ba1da570 authored by Jean-Christophe's avatar Jean-Christophe

new example from Rustan's demo of Dafny at VSTTE 2012

parent 21c2d25a
(* From Rustan Leino's tutorial on Dafny at VSTTE 2012 *)
module Fill
use import int.Int
use import module array.Array
type tree = Null | Node tree int tree
predicate contains (t: tree) (x: int) = match t with
| Null -> false
| Node l y r -> contains l x || x = y || contains r x
end
let rec fill (t: tree) (a: array int) (start: int) : int =
{ 0 <= start <= length a }
match t with
| Null ->
start
| Node l x r ->
let res = fill l a start in
if res <> length a then begin
a[res] <- x;
fill r a (res + 1)
end else
res
end
{ start <= result <= length a /\
(forall i: int. 0 <= i < start -> a[i] = (old a)[i]) /\
(forall i: int. start <= i < result -> contains t a[i]) }
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="fill/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
version="0.93.1"/>
<file
name="../fill.mlw"
verified="true"
expanded="true">
<theory
name="WP Fill"
locfile="fill/../fill.mlw"
loclnum="2" loccnumb="7" loccnume="11"
verified="true"
expanded="true">
<goal
name="WP_parameter fill"
locfile="fill/../fill.mlw"
loclnum="14" loccnumb="10" loccnume="14"
expl="parameter fill"
sum="a7f6d0a4fd8b99196978e39ff255fcf5"
proved="true"
expanded="true"
shape="CV0aNullacontainsV0agetV3V4Iainfix <V4V2Aainfix <=V2V4FAainfix =agetV3V5agetV3V5Iainfix <V5V2Aainfix <=c0V5FAainfix <=V2V1Aainfix <=V2V2aNodeVVViainfix =V10V1NacontainsV0agetV12V14Iainfix <V14V13Aainfix <=V2V14FAainfix =agetV12V15agetV3V15Iainfix <V15V2Aainfix <=c0V15FAainfix <=V13V1Aainfix <=V2V13IacontainsV8agetV12V16Iainfix <V16V13Aainfix <=ainfix +V10c1V16FAainfix =agetV12V17agetV11V17Iainfix <V17ainfix +V10c1Aainfix <=c0V17FAainfix <=V13V1Aainfix <=ainfix +V10c1V13FFAainfix <=ainfix +V10c1V1Aainfix <=c0ainfix +V10c1Iainfix =V11asetV9V10V7FAainfix <V10V1Aainfix <=c0V10acontainsV0agetV9V18Iainfix <V18V10Aainfix <=V2V18FAainfix =agetV9V19agetV3V19Iainfix <V19V2Aainfix <=c0V19FAainfix <=V10V1Aainfix <=V2V10IacontainsV6agetV9V20Iainfix <V20V10Aainfix <=V2V20FAainfix =agetV9V21agetV3V21Iainfix <V21V2Aainfix <=c0V21FAainfix <=V10V1Aainfix <=V2V10FFAainfix <=V2V1Aainfix <=c0V2Iainfix <=V2V1Aainfix <=c0V2FFFF">
<label
name="expl:parameter fill">
</label>
<proof
prover="0"
timelimit="10"
obsolete="false">
<result status="valid" time="0.15"/>
</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