--- layout: fc_discuss_archives title: Message 132 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



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