--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on December 2015 ---
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>