--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on October 2008 ---
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 |