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

  • Subject: [Frama-c-discuss] Loop Termination Challenge
  • From: Nicolas.Rousset at gemalto.com (Rousset Nicolas)
  • Date: Tue, 22 Dec 2009 11:21:02 +0100
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