--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] YASE \lambda




Unfortunately, this feature is not expected to be available in the next 
release. Indeed neither \lambda nor \sum. The only thing we can propose 
is a work-around, for providing an ad-hoc (e.g specific for each 
example) equivalent specification.

- Claude

Christoph Weber wrote:
> Salut,
> 
> I'm thinking about some stuff I found in the acsl1_3 manual. I encountered \lambda, it seems comfortable so I wonder will following example work in the next release?
> 
> /*@
>  requires last > first;
>  requires \valid_range(first, 0, last-first -1);
>  ensures  \result == \sum(0, last-first -1,(\lambda integer k ; first[k] == value ? 1 : 0)); 
> 
> */
> int count_int_array ( int* first, int* last, int value )
> {
>   int ret=0;
>   //@ ghost int* a = first;
>     /*@
>      loop invariant a <= first <= last;
>      loop invariant ret == \sum(0, first-a-1,(\lambda integer k ; first[k] == value ? 1 : 0));
>     */
>   while (first != last) if (*first++ == value) ++ret;
>   return ret;
> }
> 
> Merci d'avance
> 
> Christoph
> 
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss@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                    |