--- layout: fc_discuss_archives title: Message 87 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] unproven VC with newer why version



Thanks for the many replies.
I tried it and it worked.
At the same time I have to admit that I haven't really understood the necessity of the loop variant.

In our example we have a lot of loops the would include loop annotations of the form

	loop invariant 0 <= i <= n;
	loop    variant n-i;

Is there a way to easily combine and shorten these two lines?

Jens

Am 08.12.2009 um 14:54 schrieb Claude Marche:

> Jens Gerlach wrote:
>> We were able to deductively verify the following implementation of 
>> linear search successfully with Jessie on top of why version 2.19.
>> 
>> However, with why 2.23 there is one safety related VC that remains 
>> unproven.
>> In the jessie gui, the unproven VC reads "variant decreases".
>> 
>> Do we have to improve the specification to get rid of that issue?
>> If so, how?
> add "loop variant n-i;" and you should be done !
> 
> Since Why 2.22, the policy for generating termination VCS is as strict 
> as possible, to guarantee soundness
> (see BTS #0000103)
> 
> In the future, Jessie should support ACSL "terminates" clauses, to 
> manually annotate function for which you don;t care about termination.
> 
> In a nearer future, there could a new pragma to control the generation 
> of such VCs.
> 
> Anyway: any suggestion welcome !
> 
> - Claude
>> 
>> Regards  Jens
>> 
>> /*@
>>  requires  n >= 0;
>>  requires  \valid_range(a, 0, n-1);
>> 
>>  assigns  \nothing;
>> 
>>  behavior some:
>>    assumes  \exists int i; (0 <= i < n) && a[i] == v;
>>    ensures  0 <= \result < n;
>>    ensures  a[\result] == v;
>>    ensures  \forall int i; (0 <= i < \result) ==> a[i] != v;
>> 
>>  behavior none:
>>    assumes  \forall int i; (0 <= i < n) ==>  a[i] != v;
>>    ensures  \result == n;
>> */
>> int find(const int* a, int n, int v)
>> {
>>  /*@
>>    loop invariant 0 <= i <= n;
>>    loop invariant \forall int k; 0 <= k < i ==> a[k] != v;
>>   */
>>  for (int i = 0; i < n; ++i)
>>    if (a[i] == v)
>>      return i;
>> 
>>  return n;
>> }
>> 
>> 
>> -- 
>> 
>> Dr.-Ing. Jens Gerlach
>> Eingebettete Systeme - EST
>> Tel.: +49 (0)30 6392 1841
>> Fax.: +49 (0)30 6392 1805
>> E-Mail: jens.gerlach at first.fraunhofer.de 
>> <mailto:jens.gerlach at first.fraunhofer.de>
>> 
>> Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST
>> Kekul?stra?e 7
>> 12489 Berlin
>> Germany
>> http://www.first.fraunhofer.de
>> 
>> 
>> 
>> 
>> ------------------------------------------------------------------------
>> 
>> _______________________________________________
>> 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
> 
> 
> -- 
> Claude March?                          | tel: +33 1 72 92 59 69           
> INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
> Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
> 4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
> F-91893 ORSAY Cedex                    |
> 
> 
> 
> 
> 
> 
> 
> 
> _______________________________________________
> 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


-- 

Dr.-Ing. Jens Gerlach
Eingebettete Systeme - EST
Tel.: +49 (0)30 6392 1841
Fax.: +49 (0)30 6392 1805
E-Mail: jens.gerlach at first.fraunhofer.de

Fraunhofer-Institut f?r Rechnerarchitektur und Softwaretechnik, FIRST
Kekul?stra?e 7
12489 Berlin
Germany
http://www.first.fraunhofer.de


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091208/c547da73/attachment.htm