Software Specification: Proving Termination, Arrays, and Quantifiers

Software Specification, MEIC @ IST, 2020/21

João F. Ferreira

Proving Termination

• Because the halting problem is undecidable, termination analysis cannot be total.
• A simple, general method for constructing termination proofs involves associating a measure with each step of an algorithm. The measure is taken from a well-founded domain.
  • If the measure "decreases" in the domain along every possible step of the algorithm, it must terminate, because there are no infinite descending chains with respect to a well-founded domain.

Proving Termination

• A strict partially ordered domain is a pair $(W,\succ)$ where $W$ is a set and $\succ$ is a strict partial order relation over the set $W$
• A strict partial order relation $\succ$ satisfies for all $a$, $b$, and $c$ in $W$:
  • Irreflexivity: $a \not\succ a$
  • Transitivity: $a \succ b$ and $b \succ c$ then $a \succ c$
• A well-founded domain is a partially ordered domain that contains no infinite decreasing sequence $w_0 \succ w_1 \succ w_2 \succ \cdots$

Proving Termination

• The set of natural numbers equipped with the relation "greater than" $\gt$ is a well-founded domain.
• The set of integer numbers equipped with the relation "greater than" $\gt$ is not a well-founded domain. (Why?)
• Examples of well-founded domains:
  • The set of strings with the strict lexicographic order
  • The set of strings with the strict "superstring" relation

Proving Termination

1. Define a variant expression $v$ over a well-founded domain (e.g. $(\mathbb{N}, \gt)$)
2. Given a loop invariant $I$, prove: $$ \ht{I \wedge b \wedge v=x}{C}{x \gt v} $$ where $x$ is a fresh variable

Note: We can use integer expressions, as long as we show that they are non-negative before entering the loop body.

Proving Termination in Dafny

• Dafny proves that code terminates, i.e. does not loop forever, by using the decreases annotation.
• Dafny is usually able to guess the right annotations, but sometimes they need to be made explicit.
• There are two places Dafny proves termination: loops and recursion. Both of these situations require either an explicit annotation or a correct guess by Dafny.

while 0 < i
  invariant 0 <= i
  decreases i
{
    i := i - 1;
}

Exercise: Prove termination of the following loop:

method m1(m: int, n: int) 
requires 0 < m && 0 < n
{
    var x, y := m, n;

    while x != y
    invariant 0 < x && 0 < y
   {
      if x < y {
          y := y - x;
      } else {
          x := x - y;
      }
   }
}

Exercise: Termination annotations might be necessary when we have recursive methods or functions. Prove that the following function terminates:

function f(n: nat, m: nat): nat 
{
    if n==m then n 
    else if n<m then f(n, m-n) else f(n-m, m)
}

Arrays

• Arrays are a built-in part of Dafny. Their type is array<T>, where T is another type.
• They have similarities with arrays in mainstream languages such as Java:
  • Arrays can be null, and have a built-in length field, a.Length
  • Element access uses the standard bracket syntax and are indexed from zero: a[0], a[1], ...
• In Dafny, all array accesses must be proven to be within bounds. Because bounds checks are proven at verification time, no runtime checks need to be made.

Arrays

• Example: Searching an array for a particular key, returning the index of a place where we can find the key if it exists.
• We have two outcomes for a search:
  • If the algorithm returns an index (i.e. non-negative integer), then the key should be present at that index.
  • If the key is not in the array, then we would like the method to return a negative number. In this case, we want to say that the method did not miss an occurrence of the key; in other words, that the key is not in the array.

Exercise: Specify the first requirement of Find: if the algorithm returns an index (i.e. non-negative integer), then the key should be present at that index.

Use the following signature for your method:

method Find(a: array<int>, key: int) returns (index: int)

Exercise: Implement Find in a way that satisfies your specification.

Arrays

• To satisfy the first requirement:

  method Find(a: array<int>, key: int) returns (index: int)
  ensures 0 <= index ==> index < a.Length && a[index] == key
  {
     // ...
  }

• To satisfy the second requirement, we need to introduce quantifiers

Quantifiers

• A quantifier in Dafny most often takes the form of a forall expression, also called a universal quantifier. Example:

  forall k :: k < k + 1

• We often quantify over the elements of an array or data structure:

  forall k :: 0 <= k < a.length ==>  0 <= a[k]

• We can also write existential quantifications:

  exists k :: 0 <= k < a.length ==>  0 <= a[k]

Exercise: Use quantifiers to specify that the method Find returns a negative number whenever the searched key is not present in the array.

method Find(a: array<int>, key: int) returns (index: int)
   ensures 0 <= index ==> index < a.Length && a[index] == key
{
   // ...
}

Exercise: Write a method that takes an integer array, which it requires to have at least one element, and returns an index to the maximum of the array's elements. Annotate the method with pre- and postconditions that state the intent of the method, and annotate its body with a loop invariant to verify it.

method FindMax(a: array<int>) returns (max: int)

Credits

• These slides use the framework reveal.js and were produced using vim and Ubuntu.
• Some slides and examples are based on material available online by Rustan Leino. Some material is taken from Dafny's tutorial.