Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

kmp: proof in progress

parent 9aa2b716
......@@ -98,10 +98,10 @@ module KnuthMorrisPratt
let initnext () =
{ 1 <= length next = length p }
let m = length p in
let i = ref 1 in
let j = ref 0 in
if 1 < m then begin
next[1] <- 0;
let i = ref 1 in
let j = ref 0 in
while !i < m - 1 do
invariant { 0 <= !j <= m /\ !j < !i <= m
/\ matches p (!i - !j) p 0 !j
......@@ -109,9 +109,9 @@ module KnuthMorrisPratt
/\ (forall k:int. 0 < k <= !i -> is_next p k next[k]) }
variant { (m - !i, !j) } with lex
if p[!i] = p[!j] then begin
i := !i+1; j := !j+1; next[!i] <- !j
i := !i + 1; j := !j + 1; next[!i] <- !j
end else
if !j = 0 then begin i := !i+1; next[!i] <- 0 end else j := next[!j]
if !j = 0 then begin i := !i + 1; next[!i] <- 0 end else j := next[!j]
done
end
{ forall j:int. 0 < j < p.length -> is_next p j next[j] }
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter mark : Type.
Parameter at1: forall (a:Type), a -> mark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1)
a2) = b1).
Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| mk_array _ elts1 => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| mk_array length1 _ => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| mk_array xcl0 _ => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Parameter char : Type.
Definition matches(a1:(array char)) (i1:Z) (a2:(array char)) (i2:Z)
(n:Z): Prop := ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
(((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < n)%Z) -> ((get1 a1 (i1 + i)%Z) = (get1 a2
(i2 + i)%Z))).
Axiom matches_empty : forall (a1:(array char)) (a2:(array char)) (i1:Z)
(i2:Z), ((0%Z <= i1)%Z /\ (i1 <= (length a1))%Z) -> (((0%Z <= i2)%Z /\
(i2 <= (length a2))%Z) -> (matches a1 i1 a2 i2 0%Z)).
Axiom matches_right_extension : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z), (matches a1 i1 a2 i2 n) ->
((i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
((i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z -> (((get1 a1
(i1 + n)%Z) = (get1 a2 (i2 + n)%Z)) -> (matches a1 i1 a2 i2
(n + 1%Z)%Z)))).
Axiom matches_contradiction_at_first : forall (a1:(array char)) (a2:(array
char)) (i1:Z) (i2:Z) (n:Z), (0%Z < n)%Z -> ((~ ((get1 a1 i1) = (get1 a2
i2))) -> ~ (matches a1 i1 a2 i2 n)).
Axiom matches_contradiction_at_i : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (i:Z) (n:Z), (0%Z < n)%Z -> (((0%Z <= i)%Z /\ (i < n)%Z) ->
((~ ((get1 a1 (i1 + i)%Z) = (get1 a2 (i2 + i)%Z))) -> ~ (matches a1 i1 a2
i2 n))).
Axiom matches_right_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 i1 a2 i2 n) -> ((nqt < n)%Z ->
(matches a1 i1 a2 i2 nqt)).
Axiom matches_left_weakening : forall (a1:(array char)) (a2:(array char))
(i1:Z) (i2:Z) (n:Z) (nqt:Z), (matches a1 (i1 - (n - nqt)%Z)%Z a2
(i2 - (n - nqt)%Z)%Z n) -> ((nqt < n)%Z -> (matches a1 i1 a2 i2 nqt)).
Axiom matches_sym : forall (a1:(array char)) (a2:(array char)) (i1:Z) (i2:Z)
(n:Z), (matches a1 i1 a2 i2 n) -> (matches a2 i2 a1 i1 n).
Axiom matches_trans : forall (a1:(array char)) (a2:(array char)) (a3:(array
char)) (i1:Z) (i2:Z) (i3:Z) (n:Z), (matches a1 i1 a2 i2 n) -> ((matches a2
i2 a3 i3 n) -> (matches a1 i1 a3 i3 n)).
Definition is_next(p:(array char)) (j:Z) (n:Z): Prop := ((0%Z <= n)%Z /\
(n < j)%Z) /\ ((matches p (j - n)%Z p 0%Z n) /\ forall (z:Z),
((n < z)%Z /\ (z < j)%Z) -> ~ (matches p (j - z)%Z p 0%Z z)).
Axiom next_iteration : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((matches a (i - j)%Z p 0%Z j) -> ((is_next p j
n) -> (matches a (i - n)%Z p 0%Z n)))).
Axiom next_is_maximal : forall (p:(array char)) (a:(array char)) (i:Z) (j:Z)
(n:Z) (k:Z), ((0%Z < j)%Z /\ (j < (length p))%Z) -> (((j <= i)%Z /\
(i <= (length a))%Z) -> ((((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z) ->
((matches a (i - j)%Z p 0%Z j) -> ((is_next p j n) -> ~ (matches a k p 0%Z
(length p)))))).
Axiom next_1_0 : forall (p:(array char)), (1%Z <= (length p))%Z -> (is_next p
1%Z 0%Z).
Definition lt_nat(x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
Inductive lex : (Z* Z)%type -> (Z* Z)%type -> Prop :=
| Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1,
y1) (x2, y2))
| Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x,
y2)).
Parameter p: (array char).
Parameter next: (array Z).
Theorem WP_parameter_initnext : forall (next1:Z), forall (p1:Z),
forall (next2:(map Z Z)), forall (p2:(map Z char)), let p3 := (mk_array p1
p2) in (((1%Z <= next1)%Z /\ (next1 = p1)) -> ((1%Z < p1)%Z ->
(((0%Z <= 1%Z)%Z /\ (1%Z < next1)%Z) -> forall (next3:(map Z Z)),
(next3 = (set next2 1%Z 0%Z)) -> forall (j:Z), forall (i:Z),
forall (next4:(map Z Z)), (((0%Z <= j)%Z /\ (j <= p1)%Z) /\ (((j < i)%Z /\
(i <= p1)%Z) /\ ((matches p3 (i - j)%Z p3 0%Z j) /\ ((forall (z:Z),
(((j + 1%Z)%Z < z)%Z /\ (z < (i + 1%Z)%Z)%Z) -> ~ (matches p3
((i + 1%Z)%Z - z)%Z p3 0%Z z)) /\ forall (k:Z), ((0%Z < k)%Z /\
(k <= i)%Z) -> (is_next p3 k (get next4 k)))))) ->
((i < (p1 - 1%Z)%Z)%Z -> (((0%Z <= i)%Z /\ (i < p1)%Z) ->
(((0%Z <= j)%Z /\ (j < p1)%Z) -> (((get p2 i) = (get p2 j)) ->
forall (i1:Z), (i1 = (i + 1%Z)%Z) -> forall (j1:Z), (j1 = (j + 1%Z)%Z) ->
(((0%Z <= i1)%Z /\ (i1 < next1)%Z) -> forall (next5:(map Z Z)),
(next5 = (set next4 i1 j1)) -> forall (z:Z), (((j1 + 1%Z)%Z < z)%Z /\
(z < (i1 + 1%Z)%Z)%Z) -> ~ (matches p3 ((i1 + 1%Z)%Z - z)%Z p3 0%Z
z))))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros n n1 next1 p1.
intro p3. unfold p3. clear p3.
intros (_, eqn). subst n1. intros hn _ _ _.
intros j i next4 (hj, (hi, (h1, (h2, h3)))).
intros hi' _ _ eq.
intros i1 hi1; subst i1.
intros j1 hji1; subst j1.
intros _ _ _ z hz.
red; intro h. unfold matches, length , get1 in h. simpl in h.
destruct h as (hy1, (hy2, hy3)).
Qed.
(* DO NOT EDIT BELOW *)
......@@ -94,16 +94,56 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter initnext.6" expl="loop invariant preservation" sum="30d44d6330328364944ed659a0813add" proved="false" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="2.16"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.12"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.24"/>
</proof>
<goal name="WP_parameter initnext.6" expl="loop invariant preservation" sum="30d44d6330328364944ed659a0813add" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter initnext.6.1" expl="correctness of parameter initnext" sum="4ccdb8b3b0e1540aeed3223499c57d4f" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter initnext.6.2" expl="correctness of parameter initnext" sum="f93cdfc5669cb674ca1ae290fc1331d4" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter initnext.6.3" expl="correctness of parameter initnext" sum="09f6fa63093ccff23c6a6e268ca9d9f9" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter initnext.6.4" expl="correctness of parameter initnext" sum="c8b72addaa20143058745539f27eab57" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter initnext.6.5" expl="correctness of parameter initnext" sum="e0f2a2ca9751b8464299ee8ac84b3e8f" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="4.35"/>
</proof>
</goal>
<goal name="WP_parameter initnext.6.6" expl="correctness of parameter initnext" sum="5a7db9cfa81d5bb670deb9aa80d7a032" proved="false" expanded="true">
<proof prover="coq" timelimit="10" edited="kmp_WP_KnuthMorrisPratt_WP_parameter_initnext_1.v" obsolete="false"><undone/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="3.20"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.10"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.02"/>
</proof>
</goal>
<goal name="WP_parameter initnext.6.7" expl="correctness of parameter initnext" sum="ecf3b06606f3a9e7adce26fe58783bfd" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="5.19"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter initnext.7" expl="loop variant decreases" sum="fd63551876460009add6b997d0e9fac3" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......@@ -115,16 +155,50 @@
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter initnext.9" expl="loop invariant preservation" sum="1e0418bef822e1a76bcd3d94498d6a52" proved="false" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="2.79"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.93"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="11.00"/>
</proof>
<goal name="WP_parameter initnext.9" expl="loop invariant preservation" sum="1e0418bef822e1a76bcd3d94498d6a52" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter initnext.9.1" expl="correctness of parameter initnext" sum="54a5851daf80e2e99d2c3acbdc9a2d01" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter initnext.9.2" expl="correctness of parameter initnext" sum="40c74d7a1832f57442d4111ceb7fecbf" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter initnext.9.3" expl="correctness of parameter initnext" sum="a7b9f4ad3bd71a27628b9910293337dc" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter initnext.9.4" expl="correctness of parameter initnext" sum="700ef7340a7deae4112572d854f9aad0" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter initnext.9.5" expl="correctness of parameter initnext" sum="f338346a9fbc55baff9c8e16fc8e27a0" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter initnext.9.6" expl="correctness of parameter initnext" sum="94b97e669193d37f0d519f036f753ffd" proved="false" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="unknown" time="2.29"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.10"/>
</proof>
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.03"/>
</proof>
</goal>
<goal name="WP_parameter initnext.9.7" expl="correctness of parameter initnext" sum="028b0a3702aa0852de2313677fa72d47" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.29"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter initnext.10" expl="loop variant decreases" sum="cca350e48ed9f2d6e6bfd1e516655036" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......@@ -136,8 +210,8 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter initnext.12" expl="loop invariant preservation" sum="af8fc3f533a17a307d87903d6dd46035" proved="false" expanded="false">
<transf name="split_goal" proved="false" expanded="false">
<goal name="WP_parameter initnext.12" expl="loop invariant preservation" sum="af8fc3f533a17a307d87903d6dd46035" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter initnext.12.1" expl="correctness of parameter initnext" sum="42db1a8315d2167d40ea0763139efe3d" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
......@@ -163,7 +237,7 @@
<result status="valid" time="1.11"/>
</proof>
</goal>
<goal name="WP_parameter initnext.12.6" expl="correctness of parameter initnext" sum="c44a60846c156fb868033d1c8cebb9f0" proved="false" expanded="false">
<goal name="WP_parameter initnext.12.6" expl="correctness of parameter initnext" sum="c44a60846c156fb868033d1c8cebb9f0" proved="false" expanded="true">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.14"/>
</proof>
......@@ -202,73 +276,17 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter kmp" expl="correctness of parameter kmp" sum="3ea7bafcea60971d1305a63249d55329" proved="false" expanded="true">
<transf name="split_goal" proved="false" expanded="true">
<goal name="WP_parameter kmp" expl="correctness of parameter kmp" sum="3ea7bafcea60971d1305a63249d55329" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter kmp.1" expl="precondition" sum="061409c5a332cdf4323d8020687b1d26" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2" expl="loop invariant init" sum="68ff401a62d3fe05a8d127509cb1e5b6" proved="true" expanded="false">
<transf name="inline_goal" proved="true" expanded="false">
<goal name="WP_parameter kmp.2.1" expl="loop invariant init" sum="26ec7b72e58e63cc556cc91ed2f1743b" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter kmp.2.1.1" expl="correctness of parameter kmp" sum="4793508eae94f41396d5ee277f00bed9" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.2" expl="correctness of parameter kmp" sum="7edb65827e04c4c5bd643388967bfd99" proved="true" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.3" expl="correctness of parameter kmp" sum="4793508eae94f41396d5ee277f00bed9" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.4" expl="correctness of parameter kmp" sum="6f93320fd5c9d568a30d249a18da35ae" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.5" expl="correctness of parameter kmp" sum="d0f2ceb3e69760d2c64899f9966eec19" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.6" expl="correctness of parameter kmp" sum="3ac60e0ca5c1837067448511664ca51d" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.7" expl="correctness of parameter kmp" sum="a9b63c7da0dbe47734ee2a441f7dbedc" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.8" expl="correctness of parameter kmp" sum="e5b4af281baae4cafc3292d63d4669cc" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.9" expl="correctness of parameter kmp" sum="f7008c3e408ae1bc9ae004cf2bc02bad" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter kmp.2.1.10" expl="correctness of parameter kmp" sum="914cdf0d092982e819d398303907f2aa" proved="true" expanded="false">
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
</transf>
</goal>
</transf>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal name="WP_parameter kmp.3" expl="precondition" sum="575d6b91409f9a6370fbe5561cb8a6bd" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......@@ -311,13 +329,39 @@
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter kmp.10" expl="loop invariant preservation" sum="5ab1a22e61c0329a65732b6862762367" proved="false" expanded="false">
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.11"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.09"/>
</proof>
<goal name="WP_parameter kmp.10" expl="loop invariant preservation" sum="5ab1a22e61c0329a65732b6862762367" proved="true" expanded="false">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter kmp.10.1" expl="correctness of parameter kmp" sum="40f896133a97da5d0110d51213728569" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter kmp.10.2" expl="correctness of parameter kmp" sum="20556320e6329a86e679257c648663a5" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter kmp.10.3" expl="correctness of parameter kmp" sum="a652f18631d2e5b8a5567375a7dbae2b" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal name="WP_parameter kmp.10.4" expl="correctness of parameter kmp" sum="83492e47adfe69d4333d05c67968dd18" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter kmp.10.5" expl="correctness of parameter kmp" sum="3200af3b0e66477cc0083ff361168a22" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="1.75"/>
</proof>
</goal>
<goal name="WP_parameter kmp.10.6" expl="correctness of parameter kmp" sum="91b8494f8ff46b5bd3fc63afc10e03cf" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="3.73"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter kmp.11" expl="loop variant decreases" sum="8abf9584aab429b16efe2ff0001760e8" proved="true" expanded="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
......
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