Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Help in Loop Invariant
- Subject: [Frama-c-discuss] Help in Loop Invariant
- From: allberson85 at gmail.com (Allberson Dantas)
- Date: Mon, 7 Dec 2015 08:56:42 -0300
- In-reply-to: <22DFA027-1CF6-4F0C-AE89-4FC058B2F9D6@gmail.com>
- References: <CADH2bc9BnBf5a=jEzocLM8qg639jBZgtuQcCEzJ66=UUVpKLsg@mail.gmail.com> <22DFA027-1CF6-4F0C-AE89-4FC058B2F9D6@gmail.com>
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>
- References:
- [Frama-c-discuss] Help in Loop Invariant
- From: allberson85 at gmail.com (Allberson Dantas)
- [Frama-c-discuss] Help in Loop Invariant
- From: chan.ngo2203 at gmail.com (Chan Ngo)
- [Frama-c-discuss] Help in Loop Invariant
- Prev by Date: [Frama-c-discuss] Help in Loop Invariant
- Next by Date: [Frama-c-discuss] WP: Sodium version cannot prove a property that Neon version can prove
- Previous by thread: [Frama-c-discuss] Help in Loop Invariant
- Next by thread: [Frama-c-discuss] WP: Sodium version cannot prove a property that Neon version can prove
- Index(es):