--- layout: fc_discuss_archives title: Message 132 from Frama-C-discuss on December 2009 ---
Hello, The problem of proving termination or non-termination of loops was a topical subject on the list recently. Trying to prove termination for industrial programs, I was confronted to a third case: Loops that terminates with high probability ("Probabilistic Termination"?). Hereafter is an example I took and adapted from a real code. Consider a Random Number Generator function, which generates n numbers: /*@ requires n >= 1; @ assigns buffer[0..n - 1]; @ ensures \valid(buffer + (0..n - 1)); @*/ void generateRandomNumbers(int* buffer, int n); Assume that, for security reasons for instance, we want to avoid cases where the n numbers are all the same. We can do this like that (call generateRandomNumbers() until 2 values are different): /*@ requires n >= 1 && \valid(buffer + (0..n - 1)); @ assigns buffer[0..n - 1]; @*/ void challenge(int*buffer, int n) { while (1) { generateRandomNumbers(buffer, n); int b = *buffer; int i; /*@ loop invariant 1 <= i <= n; @ loop variant n - i; @*/ for (i = 1; i < n; i++) if (b != buffer[i]) return; } } The outer loop is expected to terminate with a high probability. I think it is an interesting challenge to find how to specify and how to verify such a program. - Nicolas Rousset -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091222/737fbaf7/attachment.htm