Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 20dcfdcd authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new example: Boyer and Moore's majority algorithm

parent 79004605
(*
Boyer and Moore’s MJRTY algorithm (1980)
Determines the majority, if any, of a multiset of n votes.
Uses at most 2n comparisons and constant extra space (3 variables).
MJRTY - A Fast Majority Vote Algorithm.
Robert S. Boyer, J Strother Moore.
In R.S. Boyer (ed.), Automated Reasoning: Essays in Honor of Woody
Bledsoe, Automated Reasoning Series, Kluwer Academic Publishers,
Dordrecht, The Netherlands, 1991, pp. 105-117.
http://www.cs.utexas.edu/users/boyer/mjrty.ps.Z
Changes from the article above:
- arrays are 0-based
- we assume the input array to have at least one element
- we use 2x <= y instead of x <= floor(y/2), which is equivalent
- we do not consider arithmetic overflows (easy, but requires an
the extra hypothesis than length a <= max_int)
*)
module Mjrty
use import int.Int
use import module ref.Refint
use import module array.Array
exception Not_found
exception Found
type candidate
type votes = array candidate
type param = (M.map int candidate, candidate)
predicate pr (p: param) (i: int) = let (m, v) = p in M.([]) m i = v
clone import int.NumOfParam with type param = param, predicate pr = pr
function numof (a: votes) (c: candidate) (l u: int) : int =
num_of (a.elts, c) l u
let mjrty (a: votes) =
{ 1 <= length a }
let n = length a in
let cand = ref a[0] in
let k = ref 0 in
for i = 0 to n-1 do (* could start at 1 with k initialized to 1 *)
invariant { 0 <= !k <= i /\
numof a !cand 0 i >= !k /\
2 * (numof a !cand 0 i - !k) <= i - !k /\
forall c: candidate. c <> !cand -> 2 * numof a c 0 i <= i - !k
}
if !k = 0 then begin
cand := a[i];
k := 1
end else if !cand = a[i] then
incr k
else
decr k
done;
if !k = 0 then raise Not_found;
try
if 2 * !k > n then raise Found;
k := 0;
for i = 0 to n-1 do
invariant { !k = numof a !cand 0 i /\ 2 * !k <= n }
if a[i] = !cand then begin
incr k;
assert { !k = numof a !cand 0 (i+1) };
if 2 * !k > n then raise Found
end
done;
raise Not_found
with Found ->
!cand
end
{ 2 * numof a result 0 (length a) > length a }
| Not_found ->
{ forall c: candidate. 2 * numof a c 0 (length a) <= length a }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/mjrty.gui"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/programs/mjrty/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93.1"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3-2.2"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="0.7"/>
<prover
id="gappa"
name="Gappa"
version="0.14.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="yices"
name="Yices"
version="1.0.13"/>
<prover
id="z3-2"
name="Z3"
version="2.13"/>
<prover
id="z3-3"
name="Z3"
version="2.13"/>
<file
name="../mjrty.mlw"
verified="true"
expanded="true">
<theory
name="WP Mjrty"
verified="true"
expanded="true">
<goal
name="WP_parameter mjrty"
expl="parameter mjrty"
sum="893efb58ace5ff2eb27ab714d85154d8"
proved="true"
expanded="true"
shape="iainfix =V2c0ainfix <=ainfix *c2anum_ofaTuple2V1V4c0V0V0Fiainfix >ainfix *c2V2V0ainfix >ainfix *c2anum_ofaTuple2V1V3c0V0V0ainfix <=ainfix *c2anum_ofaTuple2V1V7c0V0V0FIainfix <=ainfix *c2V6V0Aainfix =V6anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1Aiainfix =agetV1V8V3iainfix >ainfix *c2V9V0ainfix >ainfix *c2anum_ofaTuple2V1V3c0V0V0ainfix <=ainfix *c2V9V0Aainfix =V9anum_ofaTuple2V1V3c0ainfix +V8c1Aainfix =V9anum_ofaTuple2V1V3c0ainfix +V8c1Iainfix =V9ainfix +V6c1Fainfix <=ainfix *c2V6V0Aainfix =V6anum_ofaTuple2V1V3c0ainfix +V8c1Aainfix <V8V0Aainfix <=c0V8Iainfix <=ainfix *c2V6V0Aainfix =V6anum_ofaTuple2V1V3c0V8Iainfix <=V8ainfix -V0c1Aainfix <=c0V8FFAainfix <=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0c0Iainfix <=c0ainfix -V0c1Aainfix <=ainfix *c2anum_ofaTuple2V1V10c0V0V0FIainfix >c0ainfix -V0c1Iainfix =V5c0FIainfix <=ainfix *c2anum_ofaTuple2V1V11c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V11V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix >=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix <=V2ainfix +ainfix -V0c1c1Aainfix <=c0V2Aiainfix =V2c0ainfix <=ainfix *c2anum_ofaTuple2V1V15c0ainfix +V12c1ainfix -ainfix +V12c1V14Iainfix =V15V13NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V13c0ainfix +V12c1V14ainfix -ainfix +V12c1V14Aainfix >=anum_ofaTuple2V1V13c0ainfix +V12c1V14Aainfix <=V14ainfix +V12c1Aainfix <=c0V14Iainfix =V14c1FIainfix =V13agetV1V12FAainfix <V12V0Aainfix <=c0V12iainfix =V3agetV1V12ainfix <=ainfix *c2anum_ofaTuple2V1V17c0ainfix +V12c1ainfix -ainfix +V12c1V16Iainfix =V17V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V12c1V16ainfix -ainfix +V12c1V16Aainfix >=anum_ofaTuple2V1V3c0ainfix +V12c1V16Aainfix <=V16ainfix +V12c1Aainfix <=c0V16Iainfix =V16ainfix +V2c1Fainfix <=ainfix *c2anum_ofaTuple2V1V19c0ainfix +V12c1ainfix -ainfix +V12c1V18Iainfix =V19V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V12c1V18ainfix -ainfix +V12c1V18Aainfix >=anum_ofaTuple2V1V3c0ainfix +V12c1V18Aainfix <=V18ainfix +V12c1Aainfix <=c0V18Iainfix =V18ainfix -V2c1FAainfix <V12V0Aainfix <=c0V12Iainfix <=ainfix *c2anum_ofaTuple2V1V20c0V12ainfix -V12V2Iainfix =V20V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V12V2ainfix -V12V2Aainfix >=anum_ofaTuple2V1V3c0V12V2Aainfix <=V2V12Aainfix <=c0V2Iainfix <=V12ainfix -V0c1Aainfix <=c0V12FFFAainfix <=ainfix *c2anum_ofaTuple2V1V21c0c0ainfix -c0c0Iainfix =V21agetV1c0NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1agetV1c0c0c0c0ainfix -c0c0Aainfix >=anum_ofaTuple2V1agetV1c0c0c0c0Aainfix <=c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Aiainfix =c0c0ainfix <=ainfix *c2anum_ofaTuple2V1V22c0V0V0Fiainfix >ainfix *c2c0V0ainfix >ainfix *c2anum_ofaTuple2V1agetV1c0c0V0V0ainfix <=ainfix *c2anum_ofaTuple2V1V25c0V0V0FIainfix <=ainfix *c2V24V0Aainfix =V24anum_ofaTuple2V1agetV1c0c0ainfix +ainfix -V0c1c1Aiainfix =agetV1V26agetV1c0iainfix >ainfix *c2V27V0ainfix >ainfix *c2anum_ofaTuple2V1agetV1c0c0V0V0ainfix <=ainfix *c2V27V0Aainfix =V27anum_ofaTuple2V1agetV1c0c0ainfix +V26c1Aainfix =V27anum_ofaTuple2V1agetV1c0c0ainfix +V26c1Iainfix =V27ainfix +V24c1Fainfix <=ainfix *c2V24V0Aainfix =V24anum_ofaTuple2V1agetV1c0c0ainfix +V26c1Aainfix <V26V0Aainfix <=c0V26Iainfix <=ainfix *c2V24V0Aainfix =V24anum_ofaTuple2V1agetV1c0c0V26Iainfix <=V26ainfix -V0c1Aainfix <=c0V26FFAainfix <=ainfix *c2V23V0Aainfix =V23anum_ofaTuple2V1agetV1c0c0c0Iainfix <=c0ainfix -V0c1Aainfix <=ainfix *c2anum_ofaTuple2V1V28c0V0V0FIainfix >c0ainfix -V0c1Iainfix =V23c0FIainfix >c0ainfix -V0c1Aainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter mjrty.1"
expl="precondition"
sum="d3be0db3047c98eca85c06bc7debf437"
proved="true"
expanded="false"
shape="ainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.2"
expl="exceptional postcondition"
sum="a7168d0406220777c0aee0a90ab8ecd4"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V2c0V0V0FIainfix =c0c0Iainfix >c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.3"
expl="normal postcondition"
sum="9bb5caf34ddd04bc4f87d36e90a8f6d5"
proved="true"
expanded="false"
shape="ainfix >ainfix *c2anum_ofaTuple2V1agetV1c0c0V0V0Iainfix >ainfix *c2c0V0Iainfix =c0c0NIainfix >c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.4"
expl="exceptional postcondition"
sum="0039f0b7a0ceebc2b45f90a3e6a321ba"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V3c0V0V0FIainfix >c0ainfix -V0c1Iainfix =V2c0FIainfix >ainfix *c2c0V0NIainfix =c0c0NIainfix >c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.5"
expl="for loop initialization"
sum="15f1c58bfb23a1d22f178e97449cc239"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2V2V0Aainfix =V2anum_ofaTuple2V1agetV1c0c0c0Iainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >ainfix *c2c0V0NIainfix =c0c0NIainfix >c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.6"
expl="for loop preservation"
sum="ace8b2bd9a1a3fc4886c7f6bf7c777bf"
proved="true"
expanded="false"
shape="iainfix =agetV1V4agetV1c0iainfix >ainfix *c2V5V0ainfix >ainfix *c2anum_ofaTuple2V1agetV1c0c0V0V0ainfix <=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1agetV1c0c0ainfix +V4c1Aainfix =V5anum_ofaTuple2V1agetV1c0c0ainfix +V4c1Iainfix =V5ainfix +V3c1Fainfix <=ainfix *c2V3V0Aainfix =V3anum_ofaTuple2V1agetV1c0c0ainfix +V4c1Aainfix <V4V0Aainfix <=c0V4Iainfix <=ainfix *c2V3V0Aainfix =V3anum_ofaTuple2V1agetV1c0c0V4Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >ainfix *c2c0V0NIainfix =c0c0NIainfix >c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.7"
expl="exceptional postcondition"
sum="2198d4611a9da1b31d9ef730a4bc9f5e"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V4c0V0V0FIainfix <=ainfix *c2V3V0Aainfix =V3anum_ofaTuple2V1agetV1c0c0ainfix +ainfix -V0c1c1FIainfix <=c0ainfix -V0c1Iainfix =V2c0FIainfix >ainfix *c2c0V0NIainfix =c0c0NIainfix >c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.8"
expl="for loop initialization"
sum="00128f4ddfd3774904cc950c2eb7b47c"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V2c0c0ainfix -c0c0Iainfix =V2agetV1c0NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1agetV1c0c0c0c0ainfix -c0c0Aainfix >=anum_ofaTuple2V1agetV1c0c0c0c0Aainfix <=c0c0Aainfix <=c0c0Iainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9"
expl="for loop preservation"
sum="60122298c2a3fd24fa59fc63235e549a"
proved="true"
expanded="false"
shape="iainfix =V2c0ainfix <=ainfix *c2anum_ofaTuple2V1V7c0ainfix +V4c1ainfix -ainfix +V4c1V6Iainfix =V7V5NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V5c0ainfix +V4c1V6ainfix -ainfix +V4c1V6Aainfix >=anum_ofaTuple2V1V5c0ainfix +V4c1V6Aainfix <=V6ainfix +V4c1Aainfix <=c0V6Iainfix =V6c1FIainfix =V5agetV1V4FAainfix <V4V0Aainfix <=c0V4iainfix =V3agetV1V4ainfix <=ainfix *c2anum_ofaTuple2V1V9c0ainfix +V4c1ainfix -ainfix +V4c1V8Iainfix =V9V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V8ainfix -ainfix +V4c1V8Aainfix >=anum_ofaTuple2V1V3c0ainfix +V4c1V8Aainfix <=V8ainfix +V4c1Aainfix <=c0V8Iainfix =V8ainfix +V2c1Fainfix <=ainfix *c2anum_ofaTuple2V1V11c0ainfix +V4c1ainfix -ainfix +V4c1V10Iainfix =V11V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V10ainfix -ainfix +V4c1V10Aainfix >=anum_ofaTuple2V1V3c0ainfix +V4c1V10Aainfix <=V10ainfix +V4c1Aainfix <=c0V10Iainfix =V10ainfix -V2c1FAainfix <V4V0Aainfix <=c0V4Iainfix <=ainfix *c2anum_ofaTuple2V1V12c0V4ainfix -V4V2Iainfix =V12V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<transf
name="split_goal"
proved="true"
expanded="false">
<goal
name="WP_parameter mjrty.9.1"
expl="for loop preservation"
sum="35ff3a196d8769dc4b9ead5892fa86ed"
proved="true"
expanded="false"
shape="ainfix <V4V0Aainfix <=c0V4Iainfix =V2c0Iainfix <=ainfix *c2anum_ofaTuple2V1V5c0V4ainfix -V4V2Iainfix =V5V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.2"
expl="for loop preservation"
sum="0f0afe5152f11e14985ccb079bbe492c"
proved="true"
expanded="false"
shape="ainfix <=c0V6Iainfix =V6c1FIainfix =V5agetV1V4FIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0Iainfix <=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.3"
expl="for loop preservation"
sum="3567bc9b03d03be36a62ee7232c1b4de"
proved="true"
expanded="false"
shape="ainfix <=V6ainfix +V4c1Iainfix =V6c1FIainfix =V5agetV1V4FIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0Iainfix <=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.4"
expl="for loop preservation"
sum="32792ec40e8b4ec255057c6ecca3c30c"
proved="true"
expanded="false"
shape="ainfix >=anum_ofaTuple2V1V5c0ainfix +V4c1V6Iainfix =V6c1FIainfix =V5agetV1V4FIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0Iainfix <=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="2.50"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.5"
expl="for loop preservation"
sum="0693529a734ba0027847d810baa811e6"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V5c0ainfix +V4c1V6ainfix -ainfix +V4c1V6Iainfix =V6c1FIainfix =V5agetV1V4FIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0Iainfix <=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.29"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.6"
expl="for loop preservation"
sum="1c5ce10510702ff5abbc751cc06f88b2"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V7c0ainfix +V4c1ainfix -ainfix +V4c1V6Iainfix =V7V5NFIainfix =V6c1FIainfix =V5agetV1V4FIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0Iainfix <=ainfix *c2anum_ofaTuple2V1V8c0V4ainfix -V4V2Iainfix =V8V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="cvc3-2.2"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.7"
expl="for loop preservation"
sum="042aeaae1b47d6cc973b84eea512ec41"
proved="true"
expanded="false"
shape="ainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V5c0V4ainfix -V4V2Iainfix =V5V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.8"
expl="for loop preservation"
sum="512acbdd6bd064486ca7359f2cf39b67"
proved="true"
expanded="false"
shape="ainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.9"
expl="for loop preservation"
sum="9425334df0d71657572eebabf157fd6b"
proved="true"
expanded="false"
shape="ainfix <=V5ainfix +V4c1Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.10"
expl="for loop preservation"
sum="24513f107bcb6b35e795d222f3a58832"
proved="true"
expanded="false"
shape="ainfix >=anum_ofaTuple2V1V3c0ainfix +V4c1V5Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.94"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.11"
expl="for loop preservation"
sum="87b7781e3cf9714abbdccd97ac9e21e1"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V5ainfix -ainfix +V4c1V5Iainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.12"
expl="for loop preservation"
sum="66eda86b0430660ee643d369c1c606c0"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V6c0ainfix +V4c1ainfix -ainfix +V4c1V5Iainfix =V6V3NFIainfix =V5ainfix +V2c1FIainfix =V3agetV1V4Iainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="13"
edited=""
obsolete="false">
<result status="valid" time="6.20"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.13"
expl="for loop preservation"
sum="57739bdb8e4e91e71b5d3089335be4b6"
proved="true"
expanded="false"
shape="ainfix <=c0V5Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.14"
expl="for loop preservation"
sum="3b13a27d09c3c6b6eccc244842d5b4f2"
proved="true"
expanded="false"
shape="ainfix <=V5ainfix +V4c1Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.15"
expl="for loop preservation"
sum="209f48ffc070a4f5b5f8461a8a19c13f"
proved="true"
expanded="false"
shape="ainfix >=anum_ofaTuple2V1V3c0ainfix +V4c1V5Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.16"
expl="for loop preservation"
sum="770e73b7ca7803cb3f1bb583fc97532a"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +V4c1V5ainfix -ainfix +V4c1V5Iainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0V4ainfix -V4V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="1.57"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.9.17"
expl="for loop preservation"
sum="f0ae1fadfb1204620dadd57b71873df8"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V6c0ainfix +V4c1ainfix -ainfix +V4c1V5Iainfix =V6V3NFIainfix =V5ainfix -V2c1FIainfix =V3agetV1V4NIainfix <V4V0Aainfix <=c0V4Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V7c0V4ainfix -V4V2Iainfix =V7V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0V4V2ainfix -V4V2Aainfix >=anum_ofaTuple2V1V3c0V4V2Aainfix <=V2V4Aainfix <=c0V2Iainfix <=V4ainfix -V0c1Aainfix <=c0V4FFFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.12"/>
</proof>
</goal>
</transf>
</goal>
<goal
name="WP_parameter mjrty.10"
expl="exceptional postcondition"
sum="1c4aa0ff4caf21f8a644400116018b50"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V4c0V0V0FIainfix =V2c0Iainfix <=ainfix *c2anum_ofaTuple2V1V5c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V5V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix >=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix <=V2ainfix +ainfix -V0c1c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.11"
expl="normal postcondition"
sum="a62f9ab826ca72623c0b50445cbb6aa1"
proved="true"
expanded="false"
shape="ainfix >ainfix *c2anum_ofaTuple2V1V3c0V0V0Iainfix >ainfix *c2V2V0Iainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V4c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V4V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix >=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix <=V2ainfix +ainfix -V0c1c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.12"
expl="exceptional postcondition"
sum="e3a8d1b2eaeaa6c60b5d7862d26ef600"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2anum_ofaTuple2V1V5c0V0V0FIainfix >c0ainfix -V0c1Iainfix =V4c0FIainfix >ainfix *c2V2V0NIainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V6c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V6V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix >=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix <=V2ainfix +ainfix -V0c1c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.13"
expl="for loop initialization"
sum="23cb4c5ae2a9c018d9cc86ae30f0b4a3"
proved="true"
expanded="false"
shape="ainfix <=ainfix *c2V4V0Aainfix =V4anum_ofaTuple2V1V3c0c0Iainfix <=c0ainfix -V0c1Iainfix =V4c0FIainfix >ainfix *c2V2V0NIainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V5c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V5V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix >=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix <=V2ainfix +ainfix -V0c1c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal
name="WP_parameter mjrty.14"
expl="for loop preservation"
sum="a3b8d90adc5cd382554bbf971309fa30"
proved="true"
expanded="true"
shape="iainfix =agetV1V6V3iainfix >ainfix *c2V7V0ainfix >ainfix *c2anum_ofaTuple2V1V3c0V0V0ainfix <=ainfix *c2V7V0Aainfix =V7anum_ofaTuple2V1V3c0ainfix +V6c1Aainfix =V7anum_ofaTuple2V1V3c0ainfix +V6c1Iainfix =V7ainfix +V5c1Fainfix <=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0ainfix +V6c1Aainfix <V6V0Aainfix <=c0V6Iainfix <=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0V6Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFIainfix <=c0ainfix -V0c1Iainfix =V4c0FIainfix >ainfix *c2V2V0NIainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V8c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V8V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix >=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix <=V2ainfix +ainfix -V0c1c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter mjrty.14.1"
expl="for loop preservation"
sum="3b304ffa51a335b5162d281c733922cb"
proved="true"
expanded="false"
shape="ainfix <V6V0Aainfix <=c0V6Iainfix <=ainfix *c2V5V0Aainfix =V5anum_ofaTuple2V1V3c0V6Iainfix <=V6ainfix -V0c1Aainfix <=c0V6FFIainfix <=c0ainfix -V0c1Iainfix =V4c0FIainfix >ainfix *c2V2V0NIainfix =V2c0NIainfix <=ainfix *c2anum_ofaTuple2V1V7c0ainfix +ainfix -V0c1c1ainfix -ainfix +ainfix -V0c1c1V2Iainfix =V7V3NFAainfix <=ainfix *c2ainfix -anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2ainfix -ainfix +ainfix -V0c1c1V2Aainfix >=anum_ofaTuple2V1V3c0ainfix +ainfix -V0c1c1V2Aainfix <=V2ainfix +ainfix -V0c1c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix <c0V0Aainfix <=c0c0Iainfix <=c1V0FF">
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>