Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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