--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on December 2015 ---
Hello, For a code of such a complexity, it is likely that nobody would have the time to investigate all your code and answer a so general question as "can you tell me what is wrong". Two advices : 1) your definition of "sorted" is not the one that is easy to use, it should be /*@ predicate sorted{L}(int *a, integer i, integer j) = @ \forall integer x,y; i <= x <= y < j ==> a[x] <= a[y] ; @*/ this definition is stronger. It is indeed equivalent but it requires an induction reasoning to prove it. Thus, using your definition, the provers will have to do an inductive reasoning to prove your code, a bad idea. 2) You may have a look at the Why3 versions of mergesort, and other sort algorithms, it might give you an idea of what invariant are missing: http://toccata.lri.fr/gallery/mergesort_array.en.html Hope this helps, - Claude Le 05/12/2015 16:04, Allberson Dantas a écrit : > 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] > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss > -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Ãle-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |