--- layout: fc_discuss_archives title: Message 133 from Frama-C-discuss on December 2009 ---
> 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