--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on December 2012 ---
Hello Initisar, you source code looks difficult to read in my mail client (there are a lot of question) marks. I guess your function is related to find the largest value in an array? If so, then I can recommend a look on on Chapter 4 of ourACSL tutorial http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf Regards Jens /*@ requires \valid_range(queue,0,14); ??? assigns \nothing; ??? ensures \exists int e; 0<=e && (\forall int i; 0<=i<15 && e > queue[i]) && ( (e >= 5) || (e >= 10) ) ==> \result == 0; ??? ensures \exists int e; 0<=e && (\forall int i; 0<=i<15 && e > queue[i]) && ( (e < 5) && (e < 10) ) ==> \result == e; ??? ???? */ int find_array_max(int queue[15]){ ?int i, largest; ? largest = 0; /*@ loop variant 15 - i; ??? loop invariant 0 <= i <= 15; ??? */ ? for (i = 0; i < 15; i++) { ??? if (queue[i] > largest) ????? largest = queue[i]; ? } ? if ( (largest >= 5) || (largest >=10) ) { ??? ??? ? return 0; ? } ?? return largest; } -- Please note my new email address. Dr.-Ing. Jens Gerlach Quality for Embedded Systems (QUEST) Phone +49 (0)30 6392 1841, jens.gerlach at fokus.fraunhofer.de Fraunhofer Institute for Open Communication Systems Fraunhofer FOKUS, Kekulestrasse 7, D 12489 Berlin, Germany