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

[Frama-c-discuss] YASE \lambda



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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081017/17ef22f4/attachment.html