--- layout: fc_discuss_archives title: Message 133 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Loop Termination Challenge



> 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);

It should be requires \valid... instead of ensures \valid..., no?

> 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.

Only when n >= 2 :-)

On the same line, you should also specify the range of possible values for
the generated random numbers. In the extreme case where this range would
be limited to a single value (not very interesting, I agree) then the loop
will not terminate either.

--
Jean-Christophe