--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on March 2014 ---
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.gforge.inria.fr> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss<http://cp.mcafee.com/d/k-Kr4x8idEICzBwQsL6zBNVUTsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdK3JgvjpvW_cK9KcTjWZOW8WX7fFCzBWXP7bnhIyyHtBDBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdEI3HzzobZ8Qg6BInzGKBX5Q9kITixFtd402xoQg0eTZ9OH31BIyidIL6_f9Zc-TD> > > > > -- > Cumprimentos, > Cristiano Sousa > > _______________________________________________ > 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 >