--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on March 2014 ---
Simply remove the \forall. Then, you will have to prove that j(j+1)/2 + (j+1) == (j+1)(j+2)/2. Finally, this may require the field tactic of Coq or an SMT solver with strong non-linear arithmetics (which is uncommon). L. Le 17 mars 2014 ? 23:48, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit : > Hi, > > Thanks. I have not done a lot of annotations. I thought for all j < i, we have computed sum of 1+2+3...+j, which is j(j+1)/2. > > If this is wrong, how will you repair it? Is there a notion of built-in sum which WP understands? > > Thanks once again. > Dharma > > -----Original Message----- > From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Claude Marche > Sent: Monday, March 17, 2014 6:42 PM > To: frama-c-discuss at lists.gforge.inria.fr > Subject: Re: [Frama-c-discuss] WP Question/Bug? > > > SMT solvers like Alt-Ergo, CVC and Z3 can partly deal with non-linear integer formulas, like the one of your example. No need for interactive provers there. > > The main issue is that your annotations are wrong, e.g. a formula like > > for integer j between 0 and i, sum == j*(j+1)/2 > > cannot be valid, obviously. > > Debugging annotations is not a simple task. Maybe you could give a try at E-ACSL, which might help you to find simple errors using simple tests. > > Indeed using an interactive prover like Coq is also a good way to discover false or missing annotations. But learning Coq is not a trivial thing... > > Hope this helps, > > - Claude > > > On 03/16/2014 11:04 PM, Dharmalingam Ganesan wrote: >> Hi, >> >> I'm using WP to prove the following C program, which is intended to sum the first n natural numbers. >> >> I'm not sure how one will prove such non-linear constraints. I'm not an expert in Coq. Can any one point me to an example of how an interactive-prover can be used to prove this C program is correct? >> >> >> /*@ >> @ ensures \result == n*(n+1)/2; >> @*/ >> int sum_1_n(unsigned int n) { >> int sum = 0; >> int i = 0; >> >> /*@ >> loop invariant 0<=i<=n+1; >> >> loop invariant \forall integer j; >> 0 < j < i ==> sum == j*(j+1)/2; >> >> loop assigns i, sum; >> >> loop variant n-i; >> */ >> for(i=0; i <= n; i++) >> { >> sum +=i; >> } >> >> return sum; >> } >> >> >> >> >> >> >> [formal_verification]$ frama-c -wp sum_1_n.c [kernel] preprocessing >> with "gcc -C -E -I. sum_1_n.c" >> [wp] Running WP plugin... >> [wp] Collecting axiomatic usage >> [wp] warning: Missing RTE guards >> [wp] 8 goals scheduled >> [wp] [Alt-Ergo] Goal typed_sum_1_n_loop_inv_established : Valid (16ms) >> (6) [wp] [Alt-Ergo] Goal typed_sum_1_n_loop_inv_preserved : Valid >> (16ms) (13) [wp] [Qed] Goal typed_sum_1_n_loop_assign : Valid [wp] >> [Qed] Goal typed_sum_1_n_loop_term_decrease : Valid [wp] [Alt-Ergo] >> Goal typed_sum_1_n_loop_inv_2_established : Valid (8ms) (3) [wp] >> [Alt-Ergo] Goal typed_sum_1_n_loop_term_positive : Valid (8ms) (12) >> [wp] [Alt-Ergo] Goal typed_sum_1_n_post : Unknown (6s) [wp] [Alt-Ergo] >> Goal typed_sum_1_n_loop_inv_2_preserved : Timeout (Qed:4ms) >> [wp] Proved goals: 6 / 8 >> Qed: 2 >> Alt-Ergo: 4 (8ms-16ms) (13) (interruped: 1) (unknown: 1) >> >> >> ________________________________________ >> From: frama-c-discuss-bounces at lists.gforge.inria.fr >> [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Cristiano >> Sousa [cristiano.sousa126 at gmail.com] >> Sent: Sunday, March 16, 2014 1:07 PM >> To: Frama-C public discussion >> Subject: Re: [Frama-c-discuss] WP Question/Bug? >> >> Hi, >> >> You seem to be missing your loop variant and an invariant indicating how the 'i' variable is bound. You should add: >> >> loop invariant -1 <= i < n; >> loop variant i; >> >> With this, the generated memory safety annotations are discharged. However, your post-conditions are not. >> >> In situations like this I prefer to annotate each possible outcome of the function using different behaviors. In your case it would look like this: >> >> >> /*@ >> requires n>=0 && \valid(t+(0..n-1)); >> assigns \nothing; >> >> behavior zero_size: >> assumes n == 0; >> ensures \result == 0; >> behavior no_zero: >> assumes n > 0; >> assumes \forall integer j; 0 <= j < n ==> t[j] != 0; >> ensures \result == 0; >> behavior has_zero: >> assumes n > 0; >> assumes \exists integer j; 0 <= j < n && t[j] == 0; >> ensures t[\result] == 0; >> ensures 0 <= \result < n; >> ensures \forall integer j; j > \result && j < n ==> t[j] != 0; >> >> complete behaviors; >> disjoint behaviors; >> */ >> int get_max_index(int t[], int n) >> { >> int i = 0; >> >> /*@ >> loop invariant -1 <= i < n; >> loop invariant \forall integer j; j > i && j < n ==> \at(t[j], Pre) != 0; >> loop assigns i; >> loop variant i; >> */ >> >> for(i = n-1; i >=0 ; i--) >> { >> if(t[i] == 0) return i; >> } >> >> return 0; >> } >> >> >> The annotation are longer, but I find it much easier to understand. >> The above annotations are fully discharged using Frama-C Fluorine 2 >> and alt-ergo 0.95.1 >> >> >> >> 2014-03-16 16:12 GMT+00:00 Dharmalingam Ganesan <dganesan at fc-md.umd.edu<mailto:dganesan at fc-md.umd.edu>>: >> Hi, >> >> I do not understand why the first ensures as well as the generated valid memory access within the loop are not provable. I tried it on the latest version of Frama-c. >> >> >> /*@ logic integer max_index{L}(int* t, integer n) = >> @ (n==0) ? 0 : >> @ (t[n-1] == 0) ? n-1 : max_index(t, n-1); >> */ >> >> /*@ >> requires n>=0 && \valid(t+(0..n-1)); >> assigns \nothing; >> ensures \result == max_index(t, n); >> ensures \forall integer j; j > \result && j < n ==> t[j] != 0; */ >> int get_max_index(int t[], int n) { >> int i = 0; >> >> /*@ loop invariant \forall integer j; >> j > i && j < n ==> \at(t[j], Pre) != 0; >> >> loop assigns i; >> */ >> >> for(i = n-1; i >=0 ; i--) >> { >> if(t[i] == 0) return i; >> } >> >> return 0; >> } >> >> >> >> >> >> >> >> >> >> >> [formal_verification]$ frama-c -wp -wp-rte max_index.c [kernel] >> preprocessing with "gcc -C -E -I. max_index.c" >> [wp] Running WP plugin... >> [wp] Collecting axiomatic usage >> [rte] annotating function get_max_index [rte] annotating function main >> [wp] 14 goals scheduled [wp] [Alt-Ergo] Goal >> typed_get_max_index_assert_rte_signed_overflow : Valid (8ms) (9) [wp] >> [Alt-Ergo] Goal typed_get_max_index_loop_inv_preserved : Valid (20ms) >> (26) [wp] [Alt-Ergo] Goal typed_get_max_index_post_2 : Valid (24ms) >> (27) [wp] [Qed] Goal typed_get_max_index_loop_inv_established : Valid >> [wp] [Qed] Goal typed_get_max_index_loop_assign : Valid [wp] [Qed] >> Goal typed_get_max_index_assign_part1 : Valid (4ms) [wp] [Qed] Goal >> typed_get_max_index_assign_part2 : Valid [wp] [Alt-Ergo] Goal >> typed_get_max_index_assert_rte_signed_overflow_2 : Valid (20ms) (16) >> [wp] [Qed] Goal typed_get_max_index_assign_part3 : Valid [wp] >> [Alt-Ergo] Goal typed_get_max_index_assert_rte_mem_access : Unknown >> (1s) [wp] [Qed] Goal typed_get_max_index_assign_part4 : Valid [wp] >> [Qed] Goal typed_get_max_index_assign_part5 : Valid [wp] [Qed] Goal >> typed_main_call_get_max_index_pre : Valid [wp] [Alt-Ergo] Goal >> typed_get_max_index_post : Unknown (Qed:4ms) (6s) >> [wp] Proved goals: 12 / 14 >> Qed: 8 (4ms-4ms) >> Alt-Ergo: 4 (8ms-24ms) (27) (unknown: 2) >> >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr<mailto:Frama-c-discuss at lists.gfo >> rge.inria.fr> >> http://cp.mcafee.com/d/avndy1J5AQsLTd7bybdPtPqtTAnC67QkPqtTAnC67T6jqtT >> AnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISWPEUsCO_R-juvd78 >> W_nKnjjvoVxNxVN_BHFShhlKYPOEuvkzaT0QSyrodTV5xdVYsyMCqejtPo0c-l9QUyW01_ >> Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8K >> w0vWk8OTDoCQrLL8CMnWhEwdboL7ltbSbEiFpKB3iWq8052NEw0tLWjBm63bp4ArpudJns >> h<http://cp.mcafee.com/d/k-Kr4x8idEICzBwQsL6zBNVUTsSDtV5VxxZ5cSDtV5Vxx >> ZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdK3JgvjpvW_ >> cK9KcTjWZOW8WX7fFCzBWXP7bnhIyyHtBDBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYG >> jFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0 >> kvaAWsht00_QEhBLeNdEI3HzzobZ8Qg6BInzGKBX5Q9kITixFtd402xoQg0eTZ9OH31BIy >> idIL6_f9Zc-TD> >> >> >> >> -- >> Cumprimentos, >> Cristiano Sousa >> >> _______________________________________________ >> Frama-c-discuss mailing list >> Frama-c-discuss at lists.gforge.inria.fr >> http://cp.mcafee.com/d/FZsS73gw821J5AQsLTd7bybdPtPqtTAnC67QkPqtTAnC67T >> 6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISWPEUsCO_R-j >> uvd78W_nKnjjvoVxNxVN_BHFShhlKYPOEuvkzaT0QSCrodTV5xdVYsyMCqejtPo0c-l9QU >> yW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafB >> ite8Kw0vWk8OTDoCQrLL8CMnWhEwdboL7ltbSbEiFpKB3iWq8052NEw0tLWjBm63bp4Arp >> udKR8_qNQpU4II >> > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://cp.mcafee.com/d/FZsS820O83hJ5AQsLTd7bybdPtPqtTAnC67QkPqtTAnC67T6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISWPEUsCO_R-juvd78W_nKnjjvoVxNxVN_BHFShhlKYPOEuvkzaT0QSOrodTV5xdVYsyMCqejtPo0c-l9QUyW01_Fgzbutzw25O4Eo9GX33VkDa3JstzGKBX5Q9kITixJSeGWnIngBiPta5O5mUm-wafBite8Kw0vWk8OTDoCQrLL8CMnWhEwdboL7ltbSbEiFpKB3iWq8052NEw0tLWjBm63bp4ArpudBNzpC-Z0iC4O > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140318/cfe679eb/attachment-0001.html>