--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on December 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help in Loop Invariant



Hi everyone,

Can someone tell me what is missing in this code of merge, from mergesort?

#pragma JessieIntegerModel(math)
#pragma JessieTerminationPolicy(user)

/*@ predicate sorted{L}(int *a, integer i, integer j) =
  @   \forall integer x; i <= x < j - 1 ==> a[x] <= a[x+1] ;
  @*/

/*@ requires 0 <= lower && lower < mid && mid < upper && upper <= length &&
\valid(A+(0..length)) && \valid(B+(0..length)) && sorted(A, lower, mid) &&
sorted(A, mid, upper);

@ ensures sorted(A, lower, upper);
@*/
void merge(int A[], int B[], int lower, int mid, int upper, int length)

{

int i = lower; int j = mid; int k = 0;
/*@ loop invariant lower <= i && i <= mid;
@ loop invariant mid <= j && j <= upper;
@ loop invariant k == (i-lower)+(j-mid);
@ loop invariant sorted(B, 0, k);
@ loop invariant sorted(A, i, mid) && sorted(A, j, upper);
@ loop invariant k == 0 || ((i == mid || B[k-1] <= A[i]) && (j == upper ||
B[k-1] <= A[j]));
@ loop variant (mid - i)+(upper - j);
@*/

while (i < mid && j < upper)

{
if (A[i] <= A[j]) {
B[k] = A[i]; i++;
} else {
B[k] = A[j]; j++;
}
k++;
}
//@assert (i == mid || j == upper) && sorted(B, 0, k);
/*@ loop invariant lower <= i && i <= mid && k == (i-lower)+(j-mid);
@   loop invariant sorted(B, 0, k) && sorted(A, i, mid);
@   loop invariant k == 0 || i == mid || B[k-1] <= A[i];
@   loop variant (mid - i);
@*/
while (i < mid)
{
B[k] = A[i];
i++;
k++;
}
//@assert (i == mid) && sorted(B, 0, k);
/*@loop invariant mid <= j && j <= upper && k == (i-lower)+(j-mid);
@loop invariant sorted(B, 0, k) && sorted(A, j, upper);
@loop invariant k == 0 || j == upper || B[k-1] <= A[j];
@ loop variant (upper - j);
@*/
while (j < upper)

{ B[k] = A[j]; j++; k++; }

//@assert (i == mid && j == upper) && sorted(B, 0, k);
//@assert k == upper-lower && sorted(B, 0, upper-lower);
/*@ loop invariant lower <= lower+k && lower+k <= upper;
@   loop variant (upper - lower) - k;
@*/
for (k = 0; k < upper-lower; k++){

A[lower+k] = B[k];
}

}


-- 
Allberson Dantas

[Doutorando em Ciência da Computação - UFC]
[Analista de Sistemas do Serpro - Serviço Federal de Processamento de Dados]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151205/d7df7d5d/attachment.html>