I'm attempting to annotate the merge sort algorithm with ACSL specifications and verify its correctness using Frama-C's WP plugin, but I'm running into some issues. Below is my code:
/*@
predicate Sorted(int *t, integer lo, integer hi) =
\forall integer i, j; lo <= i <= j < hi ==> t[i] <= t[j];
*/
/*@
requires \valid(A + (0..a - 1));
requires \valid(B + (0..b - 1));
requires \valid(res + (0..a + b - 1));
requires a > 0;
requires b > 0;
requires Sorted(A, 0, a);
requires Sorted(B, 0, b);
assigns res[0..a + b - 1];
ensures Sorted(res, 0, a + b);
*/
void merge(int A[], int B[], int res[], int a, int b) {
int i = 0;
int j = 0;
int k = 0;
/*@
loop invariant 0 <= i <= a;
loop invariant 0 <= j <= b;
loop invariant k == i + j;
loop invariant 0 <= k <= a + b;
loop invariant res_sorted_1: Sorted(res, 0, k);
loop invariant less_than_A: \forall integer p; 0 <= p < k && i < a ==> res[p] <= A[i];
loop invariant less_than_B: \forall integer p; 0 <= p < k && j < a ==> res[p] <= B[j];
loop assigns i, j, k;
loop assigns res[0..a + b - 1];
*/
while (i < a && j < b) {
if (A[i] <= B[j]) {
res[k] = A[i];
k = k + 1;
i = i + 1;
}
else {
res[k] = B[j];
k = k + 1;
j = j + 1;
}
}
/*@
loop invariant 0 <= i <= a;
loop invariant k == i + j;
loop invariant 0 <= k <= a + b;
loop invariant res_sorted_2: Sorted(res, 0, k);
loop invariant less_than_A_2: \forall integer p; 0 <= p < k && i < a ==> res[p] <= A[i];
loop assigns res[0..a + b - 1];
loop assigns i, k;
*/
while (i < a) {
res[k] = A[i];
k = k + 1;
i = i + 1;
}
/*@
loop invariant 0 <= j <= b;
loop invariant k == i + j;
loop invariant 0 <= k <= a + b;
loop invariant res_sorted_3: Sorted(res, 0, k);
loop invariant less_than_B_2:\forall integer p; 0 <= p < k && j < a ==> res[p] <= B[j];
loop assigns res[0..a + b - 1];
loop assigns j, k;
*/
while (j < b) {
res[k] = B[j];
k = k + 1;
j = j + 1;
}
}
When I run frama-c -wp -wp-prover Alt-Ergo,Z3 -wp-print -wp-timeout 20 _merge.c I am getting some timeout result. I've excerpted part of the output messages:
[wp] Proved goals: 40 / 47
Qed: 25 (0.61ms-24ms-66ms)
Alt-Ergo : 14 (10ms-28ms-112ms) (670) (interrupted: 7) (cached: 21)
Z3 4.8.6: 12 (10ms-32ms-60ms) (453310) (interrupted: 7) (cached: 18)
------------------------------------------------------------
Goal Preservation of Invariant 'less_than_A' (file Benchmark/acsl-algorithms_verified/fail/_merge.c, line 27):
Let x = a + b.
Let a_1 = shift_sint32(res_0, 0).
Let a_2 = havoc(Mint_undef_0, Mint_1, a_1, x).
Let x_1 = k_3 - j_1.
Let a_3 = a_2[shift_sint32(A, x_1)].
Let a_4 = a_2[shift_sint32(B, j_1)].
Let x_2 = a + j_1.
Let x_3 = k - j.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i_1) /\ is_sint32(j) /\
is_sint32(j_1) /\ is_sint32(k) /\ is_sint32(k_1) /\ is_sint32(k_2) /\
is_sint32(k_3) /\ is_sint32(x_3) /\ is_sint32(x_1) /\ is_sint32(a_4) /\
is_sint32(a_3).
(* Heap *)
Type: (region(A.base) <= 0) /\ (region(B.base) <= 0) /\
(region(res_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i < k) /\ (k < (a + j)).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(A, 0), a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(B, 0), b).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, x).
(* Pre-condition *)
Have: 0 < a.
(* Pre-condition *)
Have: 0 < b.
(* Pre-condition *)
Have: P_Sorted(Mint_1, A, 0, a).
(* Pre-condition *)
Have: P_Sorted(Mint_1, B, 0, b).
(* Invariant *)
Have: 0 <= x.
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_1, res_0, 0, 0).
(* Invariant *)
Have: (j_1 <= k_3) /\ (k_3 <= x_2).
(* Invariant *)
Have: (j_1 <= b) /\ (0 <= j_1).
(* Invariant *)
Have: (0 <= k_3) /\ (k_3 <= x).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(a_2, res_0, 0, k_3).
(* Invariant 'less_than_A' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < k_3) ->
(a_2[shift_sint32(res_0, i_2)] <= a_3))).
(* Invariant 'less_than_B' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < k_3) -> ((j_1 < a) ->
(a_2[shift_sint32(res_0, i_2)] <= a_4)))).
(* Then *)
Have: k_3 < x_2.
(* Then *)
Have: j_1 < b.
If a_3 <= a_4
Then {
Have: (k_3 = k_1) /\ ((i_1 + j) = k_1) /\ ((i_1 + j_1) = k_1).
Have: a_2[shift_sint32(res_0, k_1) <- a_2[shift_sint32(A, i_1)]] =
Mint_0.
Have: (1 + k_1) = k.
}
Else {
Have: (k_3 = k_2) /\ ((1 + j_1) = j) /\ ((1 + k_2) = k).
Have: a_2[shift_sint32(res_0, k_2) <- a_4] = Mint_0.
}
(* Invariant *)
Have: j <= k.
(* Invariant *)
Have: (j <= b) /\ (0 <= j).
(* Invariant *)
Have: (0 <= k) /\ (k <= x).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_0, res_0, 0, k).
}
Prove: Mint_0[shift_sint32(res_0, i)] <= Mint_0[shift_sint32(A, x_3)].
Prover Z3 4.8.6 returns Timeout (Qed:67ms) (20s) (cached)
Prover Alt-Ergo returns Timeout (Qed:67ms) (20s) (cached)
------------------------------------------------------------
Goal Preservation of Invariant 'less_than_B' (file Benchmark/acsl-algorithms_verified/fail/_merge.c, line 28):
Let x = a + b.
Let a_1 = shift_sint32(res_0, 0).
Let a_2 = havoc(Mint_undef_0, Mint_1, a_1, x).
Let x_1 = k_3 - j.
Let a_3 = a_2[shift_sint32(A, x_1)].
Let a_4 = a_2[shift_sint32(B, j)].
Let x_2 = a + j.
Let x_3 = k - i_1.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i_1) /\ is_sint32(i_2) /\
is_sint32(j) /\ is_sint32(k) /\ is_sint32(k_1) /\ is_sint32(k_2) /\
is_sint32(k_3) /\ is_sint32(x_3) /\ is_sint32(x_1) /\ is_sint32(a_4) /\
is_sint32(a_3).
(* Heap *)
Type: (region(A.base) <= 0) /\ (region(B.base) <= 0) /\
(region(res_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i < k) /\ (k < (a + i_1)).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(A, 0), a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(B, 0), b).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, x).
(* Pre-condition *)
Have: 0 < a.
(* Pre-condition *)
Have: 0 < b.
(* Pre-condition *)
Have: P_Sorted(Mint_1, A, 0, a).
(* Pre-condition *)
Have: P_Sorted(Mint_1, B, 0, b).
(* Invariant *)
Have: 0 <= x.
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_1, res_0, 0, 0).
(* Invariant *)
Have: (j <= k_3) /\ (k_3 <= x_2).
(* Invariant *)
Have: (j <= b) /\ (0 <= j).
(* Invariant *)
Have: (0 <= k_3) /\ (k_3 <= x).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(a_2, res_0, 0, k_3).
(* Invariant 'less_than_A' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < k_3) ->
(a_2[shift_sint32(res_0, i_3)] <= a_3))).
(* Invariant 'less_than_B' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 < k_3) -> ((j < a) ->
(a_2[shift_sint32(res_0, i_3)] <= a_4)))).
(* Then *)
Have: k_3 < x_2.
(* Then *)
Have: j < b.
If a_3 <= a_4
Then {
Have: ((1 + k_1) = k) /\ ((1 + k_3) = k) /\ ((i_1 + j) = k) /\
((1 + i_2 + j) = k).
Have: a_2[shift_sint32(res_0, k - 1) <- a_2[shift_sint32(A, k - 1 - j)]] =
Mint_0.
}
Else {
Have: (k_3 = k_2) /\ ((i_1 + j) = k_2).
Have: a_2[shift_sint32(res_0, k_2) <- a_4] = Mint_0.
Have: (1 + k_2) = k.
}
(* Invariant *)
Have: (i_1 <= a) /\ (0 <= i_1).
(* Invariant *)
Have: (i_1 <= k) /\ (k <= (b + i_1)).
(* Invariant *)
Have: (0 <= k) /\ (k <= x).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_0, res_0, 0, k).
(* Invariant 'less_than_A' *)
Have: forall i_3 : Z. ((i_1 < a) -> ((0 <= i_3) -> ((i_3 < k) ->
(Mint_0[shift_sint32(res_0, i_3)] <= Mint_0[shift_sint32(A, i_1)])))).
}
Prove: Mint_0[shift_sint32(res_0, i)] <= Mint_0[shift_sint32(B, x_3)].
Prover Z3 4.8.6 returns Timeout (Qed:69ms) (20s) (cached)
Prover Alt-Ergo returns Timeout (Qed:69ms) (20s) (cached)
------------------------------------------------------------
Goal Preservation of Invariant 'res_sorted_1' (file Benchmark/acsl-algorithms_verified/fail/_merge.c, line 26):
Let x = i + j.
Let x_1 = a + b.
Let a_1 = shift_sint32(res_0, 0).
Let a_2 = havoc(Mint_undef_0, Mint_1, a_1, x_1).
Let x_2 = k_2 - j_1.
Let a_3 = a_2[shift_sint32(A, x_2)].
Let a_4 = a_2[shift_sint32(B, j_1)].
Let x_3 = a + j_1.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(i) /\ is_sint32(i_1) /\
is_sint32(j) /\ is_sint32(j_1) /\ is_sint32(k) /\ is_sint32(k_1) /\
is_sint32(k_2) /\ is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(a_4) /\
is_sint32(a_3).
(* Heap *)
Type: (region(A.base) <= 0) /\ (region(B.base) <= 0) /\
(region(res_0.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(A, 0), a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(B, 0), b).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, x_1).
(* Pre-condition *)
Have: 0 < a.
(* Pre-condition *)
Have: 0 < b.
(* Pre-condition *)
Have: P_Sorted(Mint_1, A, 0, a).
(* Pre-condition *)
Have: P_Sorted(Mint_1, B, 0, b).
(* Invariant *)
Have: 0 <= x_1.
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_1, res_0, 0, 0).
(* Invariant *)
Have: (j_1 <= k_2) /\ (k_2 <= x_3).
(* Invariant *)
Have: (j_1 <= b) /\ (0 <= j_1).
(* Invariant *)
Have: (0 <= k_2) /\ (k_2 <= x_1).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(a_2, res_0, 0, k_2).
(* Invariant 'less_than_A' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < k_2) ->
(a_2[shift_sint32(res_0, i_2)] <= a_3))).
(* Invariant 'less_than_B' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < k_2) -> ((j_1 < a) ->
(a_2[shift_sint32(res_0, i_2)] <= a_4)))).
(* Then *)
Have: k_2 < x_3.
(* Then *)
Have: j_1 < b.
If a_3 <= a_4
Then {
Have: (k_2 = k) /\ ((i_1 + j) = k) /\ ((i_1 + j_1) = k).
Have: a_2[shift_sint32(res_0, k) <- a_2[shift_sint32(A, i_1)]] = Mint_0.
Have: (1 + i_1) = i.
}
Else {
Have: (k_2 = k_1) /\ ((i + j_1) = k_1).
Have: a_2[shift_sint32(res_0, k_1) <- a_4] = Mint_0.
Have: (1 + j_1) = j.
}
(* Invariant *)
Have: (i <= a) /\ (0 <= i).
(* Invariant *)
Have: (j <= b) /\ (0 <= j).
(* Invariant *)
Have: (x <= x_1) /\ (0 <= x).
}
Prove: P_Sorted(Mint_0, res_0, 0, x).
Prover Z3 4.8.6 returns Timeout (Qed:69ms) (20s) (cached)
Prover Alt-Ergo returns Timeout (Qed:69ms) (20s) (cached)
------------------------------------------------------------
Goal Preservation of Invariant 'less_than_A_2' (file Benchmark/acsl-algorithms_verified/fail/_merge.c, line 50):
Let a_1 = shift_sint32(res_0, 0).
Let x = a + b.
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, x).
Let x_1 = -j.
Let x_2 = k - j.
Let a_3 = a_2[shift_sint32(A, x_2)].
Let a_4 = a_2[shift_sint32(res_0, k) <- a_3].
Let x_3 = 1 + k.
Let x_4 = a + j.
Let a_5 = havoc(Mint_undef_1, Mint_0, a_1, x).
Let x_5 = k_1 - j.
Let x_6 = 1 + k - j.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(j) /\ is_sint32(k) /\
is_sint32(k_1) /\ is_sint32(x_3) /\ is_sint32(x_2) /\ is_sint32(x_5) /\
is_sint32(x_6).
(* Heap *)
Type: (region(A.base) <= 0) /\ (region(B.base) <= 0) /\
(region(res_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i <= k) /\ ((2 + k) <= x_4).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(A, 0), a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(B, 0), b).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, x).
(* Pre-condition *)
Have: 0 < a.
(* Pre-condition *)
Have: 0 < b.
(* Pre-condition *)
Have: P_Sorted(Mint_0, A, 0, a).
(* Pre-condition *)
Have: P_Sorted(Mint_0, B, 0, b).
(* Invariant *)
Have: 0 <= x.
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_0, res_0, 0, 0).
(* Invariant *)
Have: (j <= k_1) /\ (k_1 <= x_4).
(* Invariant *)
Have: (j <= b) /\ (0 <= j).
(* Invariant *)
Have: (0 <= k_1) /\ (k_1 <= x).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(a_5, res_0, 0, k_1).
(* Invariant 'less_than_A' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k_1) -> ((k_1 < x_4) ->
(a_5[shift_sint32(res_0, i_1)] <= a_5[shift_sint32(A, x_5)])))).
(* Invariant 'less_than_B' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k_1) -> ((j < a) ->
(a_5[shift_sint32(res_0, i_1)] <= a_5[shift_sint32(B, j)])))).
If k_1 < x_4
Then { (* Else *) Have: b <= j. }
(* Invariant *)
Have: (j <= k) /\ (k <= x_4).
(* Invariant *)
Have: (0 <= k) /\ (k <= x).
(* Invariant 'res_sorted_2' *)
Have: P_Sorted(a_2, res_0, 0, k).
(* Invariant 'less_than_A_2' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k) ->
(a_2[shift_sint32(res_0, i_1)] <= a_3))).
(* Then *)
Have: k < x_4.
(* Invariant *)
Have: j <= x_3.
(* Invariant *)
Have: (k < x) /\ ((-1) <= k).
(* Invariant 'res_sorted_2' *)
Have: P_Sorted(a_4, res_0, 0, x_3).
}
Prove: a_4[shift_sint32(res_0, i)] <= a_4[shift_sint32(A, x_6)].
Prover Z3 4.8.6 returns Timeout (Qed:54ms) (20s) (cached)
Prover Alt-Ergo returns Timeout (Qed:54ms) (20s) (cached)
------------------------------------------------------------
Goal Preservation of Invariant 'less_than_B_2' (file Benchmark/acsl-algorithms_verified/fail/_merge.c, line 65):
Let a_1 = shift_sint32(res_0, 0).
Let x = a + b.
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, x).
Let x_1 = -a.
Let a_3 = a_2[shift_sint32(B, k - a)].
Let a_4 = a_2[shift_sint32(res_0, k) <- a_3].
Let x_2 = 1 + k.
Let x_3 = a + j.
Let a_5 = havoc(Mint_undef_2, Mint_0, a_1, x).
Let a_6 = shift_sint32(B, j).
Let a_7 = havoc(Mint_undef_1, Mint_0, a_1, x).
Let x_4 = -j.
Let x_5 = k_2 - j.
Let x_6 = -k_1.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(j) /\ is_sint32(k) /\
is_sint32(k_1) /\ is_sint32(k_2) /\ is_sint32(x_2) /\
is_sint32(k_1 - j) /\ is_sint32(x_5) /\ is_sint32(j + k - k_1) /\
is_sint32(1 + j + k - k_1).
(* Heap *)
Type: (region(A.base) <= 0) /\ (region(B.base) <= 0) /\
(region(res_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i <= k) /\ ((2 + j + k) <= (a + k_1)).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(A, 0), a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(B, 0), b).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, x).
(* Pre-condition *)
Have: 0 < a.
(* Pre-condition *)
Have: 0 < b.
(* Pre-condition *)
Have: P_Sorted(Mint_0, A, 0, a).
(* Pre-condition *)
Have: P_Sorted(Mint_0, B, 0, b).
(* Invariant *)
Have: 0 <= x.
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_0, res_0, 0, 0).
(* Invariant *)
Have: (j <= k_2) /\ (k_2 <= x_3).
(* Invariant *)
Have: (j <= b) /\ (0 <= j).
(* Invariant *)
Have: (0 <= k_2) /\ (k_2 <= x).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(a_7, res_0, 0, k_2).
(* Invariant 'less_than_A' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k_2) -> ((k_2 < x_3) ->
(a_7[shift_sint32(res_0, i_1)] <= a_7[shift_sint32(A, x_5)])))).
(* Invariant 'less_than_B' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k_2) -> ((j < a) ->
(a_7[shift_sint32(res_0, i_1)] <= a_7[a_6])))).
If k_2 < x_3
Then { (* Else *) Have: b <= j. }
(* Invariant *)
Have: (j <= k_1) /\ (k_1 <= x_3).
(* Invariant *)
Have: (0 <= k_1) /\ (k_1 <= x).
(* Invariant 'res_sorted_2' *)
Have: P_Sorted(a_5, res_0, 0, k_1).
(* Else *)
Have: x_3 <= k_1.
(* Invariant 'less_than_B_2' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((j < a) -> ((i_1 < x_3) ->
(a_5[shift_sint32(res_0, i_1)] <= a_5[a_6])))).
(* Invariant *)
Have: (a <= k) /\ (k <= x).
(* Invariant *)
Have: 0 <= k.
(* Invariant 'res_sorted_3' *)
Have: P_Sorted(a_2, res_0, 0, k).
(* Invariant 'less_than_B_2' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k) -> ((k < (2 * a)) ->
(a_2[shift_sint32(res_0, i_1)] <= a_3)))).
(* Then *)
Have: k < x.
(* Invariant *)
Have: a <= x_2.
(* Invariant *)
Have: (-1) <= k.
(* Invariant 'res_sorted_3' *)
Have: P_Sorted(a_4, res_0, 0, x_2).
}
Prove: a_4[shift_sint32(res_0, i)] <= a_4[shift_sint32(B, 1 + k - a)].
Prover Z3 4.8.6 returns Timeout (Qed:58ms) (20s) (cached)
Prover Alt-Ergo returns Timeout (Qed:58ms) (20s) (cached)
------------------------------------------------------------
Goal Establishment of Invariant 'less_than_B_2' (file Benchmark/acsl-algorithms_verified/fail/_merge.c, line 65):
Let x = a + j.
Let a_1 = shift_sint32(res_0, 0).
Let x_1 = a + b.
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, x_1).
Let a_3 = havoc(Mint_undef_1, Mint_0, a_1, x_1).
Let a_4 = shift_sint32(B, j).
Let x_2 = -j.
Let x_3 = k_1 - j.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(j) /\ is_sint32(k) /\
is_sint32(k_1) /\ is_sint32(k - j) /\ is_sint32(x_3).
(* Heap *)
Type: (region(A.base) <= 0) /\ (region(B.base) <= 0) /\
(region(res_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
When: (0 <= i) /\ (i < k) /\ (j < a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(A, 0), a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(B, 0), b).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, x_1).
(* Pre-condition *)
Have: 0 < a.
(* Pre-condition *)
Have: 0 < b.
(* Pre-condition *)
Have: P_Sorted(Mint_0, A, 0, a).
(* Pre-condition *)
Have: P_Sorted(Mint_0, B, 0, b).
(* Invariant *)
Have: 0 <= x_1.
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_0, res_0, 0, 0).
(* Invariant *)
Have: (j <= k_1) /\ (k_1 <= x).
(* Invariant *)
Have: (j <= b) /\ (0 <= j).
(* Invariant *)
Have: (0 <= k_1) /\ (k_1 <= x_1).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(a_3, res_0, 0, k_1).
(* Invariant 'less_than_A' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k_1) -> ((k_1 < x) ->
(a_3[shift_sint32(res_0, i_1)] <= a_3[shift_sint32(A, x_3)])))).
(* Invariant 'less_than_B' *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < k_1) ->
(a_3[shift_sint32(res_0, i_1)] <= a_3[a_4]))).
If k_1 < x
Then { (* Else *) Have: b <= j. }
(* Invariant *)
Have: (j <= k) /\ (k <= x).
(* Invariant *)
Have: (0 <= k) /\ (k <= x_1).
(* Invariant 'res_sorted_2' *)
Have: P_Sorted(a_2, res_0, 0, k).
(* Else *)
Have: x <= k.
}
Prove: a_2[shift_sint32(res_0, i)] <= a_2[a_4].
Prover Z3 4.8.6 returns Timeout (Qed:37ms) (20s) (cached)
Prover Alt-Ergo returns Timeout (Qed:37ms) (20s) (cached)
------------------------------------------------------------
Goal Preservation of Invariant 'res_sorted_3' (file Benchmark/acsl-algorithms_verified/fail/_merge.c, line 64):
Let x = a + j.
Let a_1 = shift_sint32(res_0, 0).
Let x_1 = a + b.
Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, x_1).
Let a_3 = a_2[shift_sint32(B, j)].
Let x_2 = a + j_1.
Let a_4 = havoc(Mint_undef_2, Mint_0, a_1, x_1).
Let a_5 = shift_sint32(B, j_1).
Let a_6 = havoc(Mint_undef_1, Mint_0, a_1, x_1).
Let x_3 = -j_1.
Let x_4 = k_1 - j_1.
Assume {
Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(j) /\ is_sint32(j_1) /\
is_sint32(k) /\ is_sint32(k_1) /\ is_sint32(1 + j) /\
is_sint32(k - j_1) /\ is_sint32(x_4) /\ is_sint32(j + k - j_1) /\
is_sint32(1 + j + k - j_1).
(* Heap *)
Type: (region(A.base) <= 0) /\ (region(B.base) <= 0) /\
(region(res_0.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(A, 0), a).
(* Pre-condition *)
Have: valid_rw(Malloc_0, shift_sint32(B, 0), b).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, x_1).
(* Pre-condition *)
Have: 0 < a.
(* Pre-condition *)
Have: 0 < b.
(* Pre-condition *)
Have: P_Sorted(Mint_0, A, 0, a).
(* Pre-condition *)
Have: P_Sorted(Mint_0, B, 0, b).
(* Invariant *)
Have: 0 <= x_1.
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(Mint_0, res_0, 0, 0).
(* Invariant *)
Have: (j_1 <= k_1) /\ (k_1 <= x_2).
(* Invariant *)
Have: (j_1 <= b) /\ (0 <= j_1).
(* Invariant *)
Have: (0 <= k_1) /\ (k_1 <= x_1).
(* Invariant 'res_sorted_1' *)
Have: P_Sorted(a_6, res_0, 0, k_1).
(* Invariant 'less_than_A' *)
Have: forall i : Z. ((0 <= i) -> ((i < k_1) -> ((k_1 < x_2) ->
(a_6[shift_sint32(res_0, i)] <= a_6[shift_sint32(A, x_4)])))).
(* Invariant 'less_than_B' *)
Have: forall i : Z. ((0 <= i) -> ((i < k_1) -> ((j_1 < a) ->
(a_6[shift_sint32(res_0, i)] <= a_6[a_5])))).
If k_1 < x_2
Then { (* Else *) Have: b <= j_1. }
(* Invariant *)
Have: (j_1 <= k) /\ (k <= x_2).
(* Invariant *)
Have: (0 <= k) /\ (k <= x_1).
(* Invariant 'res_sorted_2' *)
Have: P_Sorted(a_4, res_0, 0, k).
(* Else *)
Have: x_2 <= k.
(* Invariant 'less_than_B_2' *)
Have: forall i : Z. ((0 <= i) -> ((j_1 < a) -> ((i < x_2) ->
(a_4[shift_sint32(res_0, i)] <= a_4[a_5])))).
(* Invariant *)
Have: (j <= b) /\ (0 <= j).
(* Invariant *)
Have: 0 <= x.
(* Invariant 'res_sorted_3' *)
Have: P_Sorted(a_2, res_0, 0, x).
(* Invariant 'less_than_B_2' *)
Have: forall i : Z. ((0 <= i) -> ((j < a) -> ((i < x) ->
(a_2[shift_sint32(res_0, i)] <= a_3)))).
(* Then *)
Have: j < b.
(* Invariant *)
Have: (-1) <= j.
(* Invariant *)
Have: (-1) <= x.
}
Prove: P_Sorted(a_2[shift_sint32(res_0, x) <- a_3], res_0, 0, 1 + a + j).
Prover Z3 4.8.6 returns Timeout (Qed:53ms) (20s) (cached)
Prover Alt-Ergo returns Timeout (Qed:53ms) (20s) (cached)
------------------------------------------------------------
I'd like to understand how to modify existing invariants or add new specifications to make Frama-C successfully verify the implementation. Below is a verified Dafny implementation of the merge algorithm that I'm referencing:
predicate IsPermutation<T(==)>(input: seq<T>, output: seq<T>)
{
multiset(input) == multiset(output)
}
predicate Sorted(a: seq<int>)
{
forall j, k :: 0 <= j <= k < |a| ==> a[j] <= a[k]
}
predicate merged(a1: seq<int>, a2: seq<int>, b: seq<int>)
{
multiset(a1) + multiset(a2) == multiset(b)
}
method merge(a1: seq<int>, a2: seq<int>, start: int, end: int, b: array<int>)
modifies b
requires Sorted(a1)
requires Sorted(a2)
requires end - start == |a1| + |a2|
requires 0 <= start <= end <= b.Length
ensures Sorted(b[start..end])
ensures merged(a1, a2, b[start..end])
ensures forall p:: 0 <= p < start ==> old(b[p]) == b[p]
ensures forall p:: end <= p < b.Length ==> old(b[p]) == b[p]
{
assert forall xs : seq<int> :: xs[0..|xs|] == xs;
assert forall xs : seq<int>, a,b : int :: 0 <= a < b < |xs| ==> xs[a..b+1] == xs[a..b] + [xs[b]];
var a1Pos := 0;
var a2Pos := 0;
var k := start;
while k < end
invariant (start <= k && k <= end)
invariant Sorted(b[start..k])
invariant (|a1| - a1Pos) + (|a2| - a2Pos) == end - k
invariant 0 <= a1Pos <= |a1|
invariant 0 <= a2Pos <= |a2|
invariant forall i :: start <= i < k && a1Pos < |a1| ==> b[i] <= a1[a1Pos]
invariant forall i :: start <= i < k && a2Pos < |a2| ==> b[i] <= a2[a2Pos]
invariant merged(a1[0..a1Pos], a2[0..a2Pos], b[start..k])
invariant forall p:: 0 <= p < start ==> old(b[p]) == b[p]
invariant forall p:: end <= p < b.Length ==> old(b[p]) == b[p]
{
if a1Pos < |a1| && a2Pos < |a2| && a1[a1Pos] <= a2[a2Pos] {
b[k] := a1[a1Pos];
a1Pos := a1Pos + 1;
} else if a1Pos < |a1| && a2Pos < |a2| && a1[a1Pos] > a2[a2Pos] {
b[k] := a2[a2Pos];
a2Pos := a2Pos + 1;
} else if a1Pos < |a1| {
assert(a2Pos >= |a2|);
b[k] := a1[a1Pos];
a1Pos := a1Pos + 1;
} else {
assert(a1Pos >= |a1|);
b[k] := a2[a2Pos];
a2Pos := a2Pos + 1;
}
k := k + 1;
}
}
My Frama-C version is 25.0 (Manganese).
The current contract is wrong, in particular, if res and a or b overlap, it is not possible to fulfill the specification with this code. So first, one needs to specify that original and result arrays are separated memory locations.
requires \separated(&A[0..(a-1)], &B[0..(b-1)], &res[0..(a+b-1)]);
Then, the invariant less_than_B has a typo:
loop invariant less_than_B: \forall integer p; 0 <= p < k && j < a ==> res[p] <= B[j];
~~~~~~^
loop invariant less_than_B: \forall integer p; 0 <= p < k && j < b ==> res[p] <= B[j];
Same typo in less_than_B_2.
Finally, one needs to state what is not modified by the second loop and state more precise bounds for k so that WP can easily handle the last case:
//@ ghost End_l: ;
/*@ ...
loop invariant \at(k, End_l) <= k <= a + b;
...
loop invariant unchanged_beg: \forall integer p; 0 <= p < \at(k, End_l) ==> res[p] == \at(res[p], End_l);
loop invariant unchanged_end: \forall integer p; k <= p < a+b ==> res[p] == \at(res[p], End_l);
Which allows to finish the proof.
/*@
predicate Sorted(int *t, integer lo, integer hi) =
\forall integer i, j; lo <= i <= j < hi ==> t[i] <= t[j];
*/
/*@
requires \valid(A + (0..a- 1));
requires \valid(B + (0..b - 1));
requires \valid(res + (0..a + b - 1));
requires \separated(&A[0..(a-1)], &B[0..(b-1)], &res[0..(a+b-1)]);
requires a > 0;
requires b > 0;
requires Sorted(A, 0, a);
requires Sorted(B, 0, b);
assigns res[0..a + b - 1];
ensures Sorted(res, 0, a + b);
*/
void merge(int A[], int B[], int res[], int a, int b) {
int i = 0;
int j = 0;
int k = 0;
/*@
loop invariant 0 <= i <= a;
loop invariant 0 <= j <= b;
loop invariant k == i + j;
loop invariant 0 <= k <= a + b;
loop invariant res_sorted_1: Sorted(res, 0, k);
loop invariant less_than_A: \forall integer p; 0 <= p < k && i < a ==> res[p] <= A[i];
loop invariant less_than_B: \forall integer p; 0 <= p < k && j < b ==> res[p] <= B[j];
loop assigns i, j, k;
loop assigns res[0..a + b - 1];
loop variant (a + b) - k ;
*/
while (i < a && j < b) {
if (A[i] <= B[j]) {
res[k] = A[i];
k = k + 1;
i = i + 1;
}
else {
res[k] = B[j];
k = k + 1;
j = j + 1;
}
}
//@ ghost End_l: ;
/*@
loop invariant 0 <= i <= a;
loop invariant k == i + j;
loop invariant \at(k, End_l) <= k <= a + b;
loop invariant res_sorted_2: Sorted(res, 0, k);
loop invariant less_than_A_2: \forall integer p; 0 <= p < k && i < a ==> res[p] <= A[i];
loop invariant unchanged_beg: \forall integer p; 0 <= p < \at(k, End_l) ==> res[p] == \at(res[p], End_l);
loop invariant unchanged_end: \forall integer p; k <= p < a+b ==> res[p] == \at(res[p], End_l);
loop assigns res[0..a + b - 1];
loop assigns i, k;
loop variant a - i ;
*/
while (i < a) {
res[k] = A[i];
k = k + 1;
i = i + 1;
}
/*@
loop invariant 0 <= j <= b;
loop invariant k == i + j;
loop invariant 0 <= k <= a + b;
loop invariant res_sorted_3: Sorted(res, 0, k);
loop invariant less_than_B_2:\forall integer p; 0 <= p < k && j < b ==> res[p] <= B[j];
loop assigns res[0..a + b - 1];
loop assigns j, k;
loop variant b - j;
*/
while (j < b) {
res[k] = B[j];
k = k + 1;
j = j + 1;
}
}
Yet, the contract is not complete since it does not state that the elements of the original arrays are in the resulting one.