Commit cc6e8548 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

lcp/lrs : start of proofs

parent e9c57cd6
......@@ -84,17 +84,47 @@ type suffixArray = {
suffixes : array int;
}
let select (s:suffixArray) (i:int) : int = s.suffixes[i]
predicate inv(s:suffixArray) =
s.values.length = s.suffixes.length
let select (s:suffixArray) (i:int) : int
requires { inv s /\ 0 <= i < s.values.length }
ensures { result = s.suffixes[i] }
= s.suffixes[i]
use import ref.Refint
let lcp (a:array int) (x y:int) : int =
let n = a.length in
let l = ref 0 in
while x + !l < n && y + !l < n && a[x + !l] = a[y + !l] do
incr l
done;
!l
let lcp (a:array int) (x y:int) : int
requires { 0 <= x < a.length }
requires { 0 <= y < a.length }
= let n = a.length in
let l = ref 0 in
while x + !l < n && y + !l < n && a[x + !l] = a[y + !l] do
invariant { 0 <= !l }
incr l
done;
!l
let test1 () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let x = lcp arr 1 2 in
assert { x = 1 };
(* int[] brr = {1,2,3,5}; *)
let brr = Array.make 4 0 in
brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
let x = lcp brr 1 2 in
assert { x = 0 };
(* int[] crr = {1,2,3,5}; *)
let crr = Array.make 4 0 in
crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
let x = lcp crr 2 3 in
assert { x = 0 };
(* int[] drr = {1,2,3,3}; *)
let drr = Array.make 4 0 in
drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
let x = lcp drr 2 3 in
assert {x = 1}
let compare (a:array int) (x y:int) : int =
if x = y then 0 else
......@@ -125,60 +155,67 @@ let create (a:array int) : suffixArray =
sort a suf;
{ values = a; suffixes = suf }
let test1 () =
int[] arr = {1,2,2,5};
let sa = create_suffixArray arr in
let x = lcp sa 1 2 in
assert {x = ?};
int[] brr = {1,2,3,5};
let sa = create_suffixArray brr in
let x = lcp sa 1 2 in
assert {x = ?};
int[] crr = {1,2,3,5};
let sa = create_suffixArray crr in
let x = lcp sa 2 3 in
assert {x = ?};
int[] drr = {1,2,3,3};
let sa = create_suffixArray drr in
let x = lcp sa 2 3 in
assert {x = ?}
let lcp2 (s:suffixArray) (i:int) : int =
lcp s.values s.suffixes[i] s.suffixes[i-1]
let test2 () =
let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
let sa = create arr in
let x = lcp2 sa 1 in
assert {x = -1 (* TODO *)};
(* int[] brr = {1,2,3,5}; *)
let brr = Array.make 4 0 in
brr[0]<-1; brr[1]<-2; brr[2]<-3; brr[3]<-5;
let sa = create brr in
let x = lcp2 sa 1 in
assert {x = -1 (* TODO *)};
(* int[] crr = {1,2,3,5}; *)
let crr = Array.make 4 0 in
crr[0]<-1; crr[1]<-2; crr[2]<-3; crr[3]<-5;
let sa = create crr in
let x = lcp2 sa 2 in
assert {x = -1 (* TODO *)};
(* int[] drr = {1,2,3,3}; *)
let drr = Array.make 4 0 in
drr[0]<-1; drr[1]<-2; drr[2]<-3; drr[3]<-3;
let sa = create drr in
let x = lcp2 sa 2 in
assert {x = -1 (* TODO *)}
end
module LRS
let lcp (s:suffixArray) (i:int) : int =
SuffixArray.lcp s s.suffixes[i] s.suffixes[i-1]
private static int solStart = 0;
private static int solLength = 0;
private static int[] a;
public static void main(String[] args) {
a = new int[args.length];
for (int i=0; i<args.length; i++) {
a[i]=Integer.parseInt(args[i]);
}
doLRS();
System.out.println(solStart+"->"+solLength);
}
public static void doLRS() {
SuffixArray sa = new SuffixArray(a);
use import int.Int
use import ref.Ref
use import array.Array
use SuffixArray
val solStart : ref int
val solLength : ref int
let lrs (a:array int) : unit =
let sa = SuffixArray.create a in
solStart := 0;
solLength := 0;
for i=1 to a.length - 1 do
let l = SuffixArray.lcp2 sa i in
if l > !solLength then begin
solStart := SuffixArray.select sa i;
solLength := l
end
done
for (int i=1; i < a.length; i++) {
int length = sa.lcp(i);
if (length > solLength) {
solStart = sa.select(i);
solLength = length;
}
}
}
let test () =
let arr = Array.make 4 0 in
arr[0]<-7; arr[1]<-8; arr[2]<-8; arr[3]<-9;
lrs arr;
assert { !solStart = 1 };
assert { !solLength = 1 }
end
//Based on code by Robert Sedgewick and Kevin Wayne.
(* Based on code by Robert Sedgewick and Kevin Wayne. *)
<?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"/>
<file
name="../verifythis_fm2012_lcp.mlw"
verified="false"
expanded="true">
<theory
name="SuffixArray"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="77" loccnumb="7" loccnume="18"
verified="false"
expanded="true">
<goal
name="WP_parameter select"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="90" loccnumb="4" loccnume="10"
expl="VC for select"
sum="72db23fed953cddd2ef9a4a487d23418"
proved="true"
expanded="false"
shape="ainfix =agetV3V2agetV3V2Aainfix &lt;V2V1Aainfix &lt;=c0V2Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix =V0V1FF">
<label
name="expl:VC for select"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter lcp"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="97" loccnumb="4" loccnume="7"
expl="VC for lcp"
sum="37c889a5d79659ff2d4ec5dde34b0c40"
proved="true"
expanded="false"
shape="ainfix &lt;=c0V5Iainfix =V5ainfix +V4c1FIainfix =agetV3ainfix +V1V4agetV3ainfix +V2V4Aainfix &lt;ainfix +V1V4V0Aainfix &lt;=c0ainfix +V1V4Aainfix &lt;ainfix +V2V4V0Aainfix &lt;=c0ainfix +V2V4Iainfix &lt;ainfix +V2V4V0Iainfix &lt;ainfix +V1V4V0Iainfix &lt;=c0V4FAainfix &lt;=c0c0Iainfix &lt;V2V0Aainfix &lt;=c0V2Aainfix &lt;V1V0Aainfix &lt;=c0V1FF">
<label
name="expl:VC for lcp"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="VC for test1"
sum="3c6add7c3520c9121972b566e9a358ec"
proved="false"
expanded="false"
shape="ainfix =V19c1FAainfix &lt;c3c4Aainfix &lt;=c0c3Aainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V18asetV17c3c3FAainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V17asetV16c2c3FAainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V16asetV15c1c2FAainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V15asetaconstc0c0c1FAainfix &lt;c0c4Aainfix &lt;=c0c0Aainfix &gt;=c4c0Aainfix =V14c0FAainfix &lt;c3c4Aainfix &lt;=c0c3Aainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V13asetV12c3c5FAainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V12asetV11c2c3FAainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V11asetV10c1c2FAainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V10asetaconstc0c0c1FAainfix &lt;c0c4Aainfix &lt;=c0c0Aainfix &gt;=c4c0Aainfix =V9c0FAainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V8asetV7c3c5FAainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FAainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FAainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FAainfix &lt;c0c4Aainfix &lt;=c0c0Aainfix &gt;=c4c0Aainfix =V4c1FAainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FAainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FAainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FAainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FAainfix &lt;c0c4Aainfix &lt;=c0c0Aainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<transf
name="split_goal_wp"
proved="false"
expanded="false">
<goal
name="WP_parameter test1.1"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="1. precondition"
sum="7b260b7ac86e413d522d49fb3f9d9c7b"
proved="true"
expanded="false"
shape="ainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1.2"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="2. precondition"
sum="afcfda21c4162e4cd3e14aec0a2317b4"
proved="true"
expanded="false"
shape="ainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1.3"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="3. precondition"
sum="63727a9716eadb90f1ea0642128260b3"
proved="true"
expanded="false"
shape="ainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1.4"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="4. precondition"
sum="8b06625cee99ec156749d80d580ced3f"
proved="true"
expanded="false"
shape="ainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1.5"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="5. precondition"
sum="3f0d9aa3eace0438476e561558859fe7"
proved="true"
expanded="false"
shape="ainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1.6"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="6. precondition"
sum="9b922d464c659bf420124b3421c098a4"
proved="false"
expanded="false"
shape="ainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
</goal>
<goal
name="WP_parameter test1.7"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="7. precondition"
sum="2083127cb96e4c5f2714b9e6d031f9e7"
proved="false"
expanded="false"
shape="ainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
</goal>
<goal
name="WP_parameter test1.8"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="8. assertion"
sum="61e6773751ac9469e81fda7aa34fd988"
proved="false"
expanded="false"
shape="ainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1.9"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="9. precondition"
sum="6e4a11ce7c1508cc1e8555e7f841efcd"
proved="true"
expanded="false"
shape="ainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1.10"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="10. precondition"
sum="8db2a92490eb01b75db212d14e811610"
proved="true"
expanded="false"
shape="ainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter test1.11"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="11. precondition"
sum="60bd6d2e0cba9954c7d7f7e3718c937b"
proved="true"
expanded="false"
shape="ainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1.12"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="12. precondition"
sum="a654cb68cabd8a1cf5edca339bf887ee"
proved="true"
expanded="false"
shape="ainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1.13"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="13. precondition"
sum="c83a92e50f04d710a7252d6fb06b9050"
proved="true"
expanded="false"
shape="ainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1.14"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="14. precondition"
sum="daaae8b7c43d2b8a367c6fc0263cb0a3"
proved="false"
expanded="false"
shape="ainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V8asetV7c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
</goal>
<goal
name="WP_parameter test1.15"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="15. precondition"
sum="44ad203573e59260aa897498e9339771"
proved="false"
expanded="false"
shape="ainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V8asetV7c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
</goal>
<goal
name="WP_parameter test1.16"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="16. assertion"
sum="17816492658709cd96e9e3b1f6a40a06"
proved="false"
expanded="false"
shape="ainfix =V9c0FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V8asetV7c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1.17"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="17. precondition"
sum="f08ab89a4f049d24452f6d330bcd9b9b"
proved="true"
expanded="false"
shape="ainfix &gt;=c4c0Iainfix =V9c0FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V8asetV7c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter test1.18"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="18. precondition"
sum="56a67aa08fd350c0e47fb385d92f6f04"
proved="true"
expanded="false"
shape="ainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V9c0FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V8asetV7c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter test1.19"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="19. precondition"
sum="52bc728793b2554b09a3169126d31fd6"
proved="true"
expanded="false"
shape="ainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V10asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V9c0FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V8asetV7c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter test1.20"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="108" loccnumb="4" loccnume="9"
expl="20. precondition"
sum="c074cb11357a20cc8950cf7a71504ba2"
proved="true"
expanded="false"
shape="ainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V11asetV10c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V10asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V9c0FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V8asetV7c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V7asetV6c2c3FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V6asetV5c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V5asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0Iainfix =V4c1FIainfix &lt;c2c4Aainfix &lt;=c0c2Aainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V3asetV2c3c5FIainfix &lt;c3c4Aainfix &lt;=c0c3Iainfix =V2asetV1c2c2FIainfix &lt;c2c4Aainfix &lt;=c0c2Iainfix =V1asetV0c1c2FIainfix &lt;c1c4Aainfix &lt;=c0c1Iainfix =V0asetaconstc0c0c1FIainfix &lt;c0c4Aainfix &lt;=c0c0Iainfix &gt;=c4c0">
<label
name="expl:VC for test1"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"