Frama-C-discuss mailing list archives

loic.correnson at cea.fr (Loïc Correnson) · Tue, 18 Mar 2014 17:32:07 +0100

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>