--- layout: fc_discuss_archives title: Message 4 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



Thanks a lot.

2015-12-07 6:34 GMT-03:00 Chan Ngo <chan.ngo2203 at gmail.com>:

> 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
>
> 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
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>



-- 
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/20151207/b9707df7/attachment.html>