Commit 7e909f86 authored by Jean-Christophe's avatar Jean-Christophe

new example: distance (in progress)

parent 0ec3c954
(*
Author: Jean-Christophe Filliatre (CNRS)
Tool: Why3 (see http://why3.lri.fr/)
The following problem was suggested to me by Ernie Cohen (Microsoft Research)
We are given an integer N>0 and a function f such that 0 <= f(i) < i
for all i in 0..N-1. We define a reachability as follows:
each integer i in 0..N-1 can be reached from any integer in f(i)..i-1
in one step.
The problem is then to compute the distance from 0 to N-1 in O(N).
Even better, we want to compute this distance, say d, for all i
in 0..N-1 and to build a predecessor function g such that
i <-- g(i) <-- g(g(i)) <-- ... <-- 0
is the path of length d[i] from 0 to i.
*)
module Distance
use import int.Int
use import module ref.Refint
use import module array.Array
(* parameters [N] and [f] are introduced as logic symbols *)
constant n: int
axiom n_nonneg: 0 < n
function f int: int
axiom f_prop: forall k: int. 0 <= k < n -> 0 <= f k < k
(* path from 0 to i of distance d *)
inductive path int int =
| path0: path 0 0
| paths: forall i: int. 0 <= i < n ->
forall d j: int. path d j -> f i <= j < i -> path (d+1) i
predicate distance (d i: int) =
path d i /\ forall d': int. path d' i -> d <= d'
(* function [g] is built in an array and then returned *)
let distance () =
{ }
let g = make n 0 in
g[0] <- -1; (* sentinel *)
let d = make n 0 in
d[0] <- 0; (* redundant *)
let count = ref 0 in (* ghost *)
for i = 1 to n-1 do
invariant { g[0] = -1 /\
(forall k: int. 0 < k < i -> f k <= g[k] < k) /\
(forall k: int. 0 < k < i -> d[k] = d[g[k]] + 1) (* /\
(forall k: int. 0 <= k < i -> path d[k] k) *) }
let j = ref (i-1) in
while g[!j] >= f i do
invariant { f i <= !j < i }
variant { !j }
j := g[!j];
incr count
done;
d[i] <- 1 + d[!j];
g[i] <- !j
done;
g
{ forall k: int. 0 < k < n -> f k <= result[k] < k }
end
(*
Local Variables:
compile-command: "why3ide distance.mlw"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/jc/why3/share/why3session.dtd">
<why3session
name="distance/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Z3"
version="3.2"/>
<file
name="../distance.mlw"
verified="true"
expanded="true">
<theory
name="WP Distance"
locfile="distance/../distance.mlw"
loclnum="22" loccnumb="7" loccnume="15"
verified="true"
expanded="true">
<goal
name="WP_parameter distance"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="parameter distance"
sum="bb8e96d780f89ee7fae2c061993c1ea4"
proved="true"
expanded="true"
shape="ainfix &lt;agetV3V4V4Aainfix &lt;=afV4agetV3V4Iainfix &lt;V4anAainfix &lt;c0V4FIainfix =agetV2V5ainfix +agetV2agetV3V5c1Iainfix &lt;V5ainfix +ainfix -anc1c1Aainfix &lt;c0V5FAainfix &lt;agetV3V6V6Aainfix &lt;=afV6agetV3V6Iainfix &lt;V6ainfix +ainfix -anc1c1Aainfix &lt;c0V6FAainfix =agetV3c0aprefix -c1Aiainfix &gt;=agetV3V8afV7ainfix &lt;V10V8Aainfix &lt;=c0V8Aainfix &lt;V10V7Aainfix &lt;=afV7V10Iainfix =V11ainfix +V9c1FIainfix =V10agetV3V8FAainfix &lt;V8anAainfix &lt;=c0V8ainfix =agetV12V14ainfix +agetV12agetV13V14c1Iainfix &lt;V14ainfix +V7c1Aainfix &lt;c0V14FAainfix &lt;agetV13V15V15Aainfix &lt;=afV15agetV13V15Iainfix &lt;V15ainfix +V7c1Aainfix &lt;c0V15FAainfix =agetV13c0aprefix -c1Iainfix =V13asetV3V7V8FAainfix &lt;V7anAainfix &lt;=c0V7Iainfix =V12asetV2V7ainfix +c1agetV2V8FAainfix &lt;V7anAainfix &lt;=c0V7Aainfix &lt;V8anAainfix &lt;=c0V8Aainfix &lt;V8anAainfix &lt;=c0V8Iainfix &lt;V8V7Aainfix &lt;=afV7V8FFAainfix &lt;ainfix -V7c1V7Aainfix &lt;=afV7ainfix -V7c1Iainfix =agetV2V16ainfix +agetV2agetV3V16c1Iainfix &lt;V16V7Aainfix &lt;c0V16FAainfix &lt;agetV3V17V17Aainfix &lt;=afV17agetV3V17Iainfix &lt;V17V7Aainfix &lt;c0V17FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V7ainfix -anc1Aainfix &lt;=c1V7FFFAainfix =agetV1V18ainfix +agetV1agetV0V18c1Iainfix &lt;V18c1Aainfix &lt;c0V18FAainfix &lt;agetV0V19V19Aainfix &lt;=afV19agetV0V19Iainfix &lt;V19c1Aainfix &lt;c0V19FAainfix =agetV0c0aprefix -c1Iainfix &lt;=c1ainfix -anc1Aainfix &lt;agetV0V20V20Aainfix &lt;=afV20agetV0V20Iainfix &lt;V20anAainfix &lt;c0V20FIainfix &gt;c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FAainfix &lt;c0anAainfix &lt;=c0c0Aainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FAainfix &lt;c0anAainfix &lt;=c0c0Aainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter distance.1"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="precondition"
sum="ea554b9905c2f687031da1fbcbc500ea"
proved="true"
expanded="false"
shape="ainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.2"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="precondition"
sum="f5480fd333bd70ab7d0cb4148288cfa1"
proved="true"
expanded="false"
shape="ainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.3"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="precondition"
sum="248f5af29241293a670301ca108ee284"
proved="true"
expanded="false"
shape="ainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.4"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="precondition"
sum="c92cdc328c8dfcd607fce4bdf0b20693"
proved="true"
expanded="false"
shape="ainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.5"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="normal postcondition"
sum="b5ffe52115a0c532dabface1283d86c5"
proved="true"
expanded="false"
shape="ainfix &lt;agetV0V2V2Aainfix &lt;=afV2agetV0V2Iainfix &lt;V2anAainfix &lt;c0V2FIainfix &gt;c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.6"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop initialization"
sum="b9aa56782bd1c231858d7573267db54c"
proved="true"
expanded="false"
shape="ainfix =agetV1V2ainfix +agetV1agetV0V2c1Iainfix &lt;V2c1Aainfix &lt;c0V2FAainfix &lt;agetV0V3V3Aainfix &lt;=afV3agetV0V3Iainfix &lt;V3c1Aainfix &lt;c0V3FAainfix =agetV0c0aprefix -c1Iainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="4f9eee320cc80d4ada8aafd57c3bd2e4"
proved="true"
expanded="true"
shape="iainfix &gt;=agetV3V5afV4ainfix &lt;V7V5Aainfix &lt;=c0V5Aainfix &lt;V7V4Aainfix &lt;=afV4V7Iainfix =V8ainfix +V6c1FIainfix =V7agetV3V5FAainfix &lt;V5anAainfix &lt;=c0V5ainfix =agetV9V11ainfix +agetV9agetV10V11c1Iainfix &lt;V11ainfix +V4c1Aainfix &lt;c0V11FAainfix &lt;agetV10V12V12Aainfix &lt;=afV12agetV10V12Iainfix &lt;V12ainfix +V4c1Aainfix &lt;c0V12FAainfix =agetV10c0aprefix -c1Iainfix =V10asetV3V4V5FAainfix &lt;V4anAainfix &lt;=c0V4Iainfix =V9asetV2V4ainfix +c1agetV2V5FAainfix &lt;V4anAainfix &lt;=c0V4Aainfix &lt;V5anAainfix &lt;=c0V5Aainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFAainfix &lt;ainfix -V4c1V4Aainfix &lt;=afV4ainfix -V4c1Iainfix =agetV2V13ainfix +agetV2agetV3V13c1Iainfix &lt;V13V4Aainfix &lt;c0V13FAainfix &lt;agetV3V14V14Aainfix &lt;=afV14agetV3V14Iainfix &lt;V14V4Aainfix &lt;c0V14FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter distance.7.1"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="fbeb12801b46e4c3143fdef2cdaad472"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -V4c1V4Aainfix &lt;=afV4ainfix -V4c1Iainfix =agetV2V5ainfix +agetV2agetV3V5c1Iainfix &lt;V5V4Aainfix &lt;c0V5FAainfix &lt;agetV3V6V6Aainfix &lt;=afV6agetV3V6Iainfix &lt;V6V4Aainfix &lt;c0V6FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<transf
name="split_goal"
proved="true"
expanded="false">
<goal
name="WP_parameter distance.7.1.1"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="273dee09ffcd0749036284dffb29c40d"
proved="true"
expanded="false"
shape="ainfix &lt;=afV4ainfix -V4c1Iainfix =agetV2V5ainfix +agetV2agetV3V5c1Iainfix &lt;V5V4Aainfix &lt;c0V5FAainfix &lt;agetV3V6V6Aainfix &lt;=afV6agetV3V6Iainfix &lt;V6V4Aainfix &lt;c0V6FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.1.2"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="8c4c77bb56963a42faa15eb7b271f662"
proved="true"
expanded="false"
shape="ainfix &lt;ainfix -V4c1V4Iainfix =agetV2V5ainfix +agetV2agetV3V5c1Iainfix &lt;V5V4Aainfix &lt;c0V5FAainfix &lt;agetV3V6V6Aainfix &lt;=afV6agetV3V6Iainfix &lt;V6V4Aainfix &lt;c0V6FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter distance.7.2"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="99a88cde834628a80d1c89969e1d7549"
proved="true"
expanded="false"
shape="ainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V7ainfix +agetV2agetV3V7c1Iainfix &lt;V7V4Aainfix &lt;c0V7FAainfix &lt;agetV3V8V8Aainfix &lt;=afV8agetV3V8Iainfix &lt;V8V4Aainfix &lt;c0V8FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.3"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="9b1ba18ba485a78bd2b68f0fc41b6d50"
proved="true"
expanded="true"
shape="ainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V7ainfix +agetV2agetV3V7c1Iainfix &lt;V7V4Aainfix &lt;c0V7FAainfix &lt;agetV3V8V8Aainfix &lt;=afV8agetV3V8Iainfix &lt;V8V4Aainfix &lt;c0V8FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.4"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="f7c5e3fa114d306f0c9bf9c5806c63ef"
proved="true"
expanded="false"
shape="ainfix &lt;V7V4Aainfix &lt;=afV4V7Iainfix =V8ainfix +V6c1FIainfix =V7agetV3V5FIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V9ainfix +agetV2agetV3V9c1Iainfix &lt;V9V4Aainfix &lt;c0V9FAainfix &lt;agetV3V10V10Aainfix &lt;=afV10agetV3V10Iainfix &lt;V10V4Aainfix &lt;c0V10FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.5"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="b1f65e425686ab104a2c7f591fff68a8"
proved="true"
expanded="false"
shape="ainfix &lt;V7V5Aainfix &lt;=c0V5Iainfix &lt;V7V4Aainfix &lt;=afV4V7Iainfix =V8ainfix +V6c1FIainfix =V7agetV3V5FIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V9ainfix +agetV2agetV3V9c1Iainfix &lt;V9V4Aainfix &lt;c0V9FAainfix &lt;agetV3V10V10Aainfix &lt;=afV10agetV3V10Iainfix &lt;V10V4Aainfix &lt;c0V10FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.6"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="f91fc49af8558b6ca3767b05817c56d8"
proved="true"
expanded="false"
shape="ainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V7ainfix +agetV2agetV3V7c1Iainfix &lt;V7V4Aainfix &lt;c0V7FAainfix &lt;agetV3V8V8Aainfix &lt;=afV8agetV3V8Iainfix &lt;V8V4Aainfix &lt;c0V8FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.7"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="84c776f3b2f2f5f28e252063e16f2335"
proved="true"
expanded="false"
shape="ainfix &lt;V4anAainfix &lt;=c0V4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V7ainfix +agetV2agetV3V7c1Iainfix &lt;V7V4Aainfix &lt;c0V7FAainfix &lt;agetV3V8V8Aainfix &lt;=afV8agetV3V8Iainfix &lt;V8V4Aainfix &lt;c0V8FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.8"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="bf961a340d233bca65f09beb21612ab6"
proved="true"
expanded="false"
shape="ainfix &lt;V4anAainfix &lt;=c0V4Iainfix =V7asetV2V4ainfix +c1agetV2V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V8ainfix +agetV2agetV3V8c1Iainfix &lt;V8V4Aainfix &lt;c0V8FAainfix &lt;agetV3V9V9Aainfix &lt;=afV9agetV3V9Iainfix &lt;V9V4Aainfix &lt;c0V9FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.9"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="cda84ed1e860a0166964e2ff8a983c53"
proved="true"
expanded="false"
shape="ainfix =agetV8c0aprefix -c1Iainfix =V8asetV3V4V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix =V7asetV2V4ainfix +c1agetV2V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V9ainfix +agetV2agetV3V9c1Iainfix &lt;V9V4Aainfix &lt;c0V9FAainfix &lt;agetV3V10V10Aainfix &lt;=afV10agetV3V10Iainfix &lt;V10V4Aainfix &lt;c0V10FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<transf
name="split_goal"
proved="true"
expanded="false">
<goal
name="WP_parameter distance.7.9.1"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="cda84ed1e860a0166964e2ff8a983c53"
proved="true"
expanded="false"
shape="ainfix =agetV8c0aprefix -c1Iainfix =V8asetV3V4V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix =V7asetV2V4ainfix +c1agetV2V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V9ainfix +agetV2agetV3V9c1Iainfix &lt;V9V4Aainfix &lt;c0V9FAainfix &lt;agetV3V10V10Aainfix &lt;=afV10agetV3V10Iainfix &lt;V10V4Aainfix &lt;c0V10FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter distance.7.10"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="117e6d5cb7e2cdd4e01cab7054c63635"
proved="true"
expanded="false"
shape="ainfix &lt;=afV9agetV8V9Iainfix &lt;V9ainfix +V4c1Aainfix &lt;c0V9FIainfix =V8asetV3V4V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix =V7asetV2V4ainfix +c1agetV2V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V10ainfix +agetV2agetV3V10c1Iainfix &lt;V10V4Aainfix &lt;c0V10FAainfix &lt;agetV3V11V11Aainfix &lt;=afV11agetV3V11Iainfix &lt;V11V4Aainfix &lt;c0V11FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.11"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="4bd531695ccc0848be0928670ce622f8"
proved="true"
expanded="false"
shape="ainfix &lt;agetV8V9V9Iainfix &lt;V9ainfix +V4c1Aainfix &lt;c0V9FIainfix =V8asetV3V4V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix =V7asetV2V4ainfix +c1agetV2V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V10ainfix +agetV2agetV3V10c1Iainfix &lt;V10V4Aainfix &lt;c0V10FAainfix &lt;agetV3V11V11Aainfix &lt;=afV11agetV3V11Iainfix &lt;V11V4Aainfix &lt;c0V11FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter distance.7.12"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="for loop preservation"
sum="d7512614ba169d7b82f7298b15830924"
proved="true"
expanded="false"
shape="ainfix =agetV7V9ainfix +agetV7agetV8V9c1Iainfix &lt;V9ainfix +V4c1Aainfix &lt;c0V9FIainfix =V8asetV3V4V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix =V7asetV2V4ainfix +c1agetV2V5FIainfix &lt;V4anAainfix &lt;=c0V4Iainfix &lt;V5anAainfix &lt;=c0V5Iainfix &gt;=agetV3V5afV4NIainfix &lt;V5anAainfix &lt;=c0V5Iainfix &lt;V5V4Aainfix &lt;=afV4V5FFIainfix =agetV2V10ainfix +agetV2agetV3V10c1Iainfix &lt;V10V4Aainfix &lt;c0V10FAainfix &lt;agetV3V11V11Aainfix &lt;=afV11agetV3V11Iainfix &lt;V11V4Aainfix &lt;c0V11FAainfix =agetV3c0aprefix -c1Iainfix &lt;=V4ainfix -anc1Aainfix &lt;=c1V4FFFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter distance.8"
locfile="distance/../distance.mlw"
loclnum="45" loccnumb="6" loccnume="14"
expl="normal postcondition"
sum="171d0b991741be22ec71e9be8b76a8aa"
proved="true"
expanded="false"
shape="ainfix &lt;agetV3V4V4Aainfix &lt;=afV4agetV3V4Iainfix &lt;V4anAainfix &lt;c0V4FIainfix =agetV2V5ainfix +agetV2agetV3V5c1Iainfix &lt;V5ainfix +ainfix -anc1c1Aainfix &lt;c0V5FAainfix &lt;agetV3V6V6Aainfix &lt;=afV6agetV3V6Iainfix &lt;V6ainfix +ainfix -anc1c1Aainfix &lt;c0V6FAainfix =agetV3c0aprefix -c1FFIainfix &lt;=c1ainfix -anc1Iainfix =V1asetaconstc0c0c0FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0Iainfix =V0asetaconstc0c0aprefix -c1FIainfix &lt;c0anAainfix &lt;=c0c0Iainfix &gt;=anc0">
<label
name="expl:parameter distance"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
</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