--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on December 2015 ---
Hi, I think that you should look at the merge sort example of Why3. For example, here is one http://pauillac.inria.fr/~levy/talks/14lc60/lc60-4.pdf <http://pauillac.inria.fr/~levy/talks/14lc60/lc60-4.pdf> Alternatively, since the invariants and assertions are in Hoare logic, so it should be good to look at how pre- and postconditions, and invariant for loops are established. Best, Chan > On Dec 5, 2015, at 4:04 PM, Allberson Dantas <allberson85 at gmail.com> wrote: > > 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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20151207/14304ee8/attachment.html>