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