Specifications and Correctness

Let’s consider the function indexOf whose purpose is to return the position of an integer element elt in a list of integers lst. In Python we might write indexOf as a recursive function:

def indexOf(lst, elt):
    if lst[0] == elt:
        return 0
    elif len(lst) == 1:
        return -1
    else:
        restidx = indexOf(lst[1:], elt)
        return restidx + 1 if restidx != -1 else -1

Is this code correct?

Testing

Testing is by far the most widely used technique that software engineers employ to answer this question. You have experience with testing from 6.101, although for the most part course staff did the most challenging and interesting part of testing: choosing test cases that, if they pass, give you a high degree of confidence that your program is not merely correct for those particular test cases but is correct in general. In order to do so, you must consider all the different ways the program’s computation might unfold: in indexOf, if we never test any inputs where we reach the len(lst) == 1 condition and it is True, we’ve left a pretty clear place in the code for bugs to hang out.

In this course, we aim directly at correct in general by writing and validating proofs of correctness. But the ability to think about different ways the computation will proceed is no less important: if we fail, in our proof, to consider what happens when we find that len(lst) == 1, then we might be able to prove some things about the behavior of indexOf but perhaps not everything we ought to.

And taking this course will be excellent preparation for working on software projects that are not using formal verification, and are using testing, precisely because you will have exercised very thoroughly this essential skill.

Code review

It’s easy to overlook bugs in your own code, but another time-honored way to find them is to get someone else to look. This practice is called code review. In serious industry projects, it is common that every chunk of new code is required to be reviewed by someone else before it can start being used for real. MIT’s 6.102 includes a big component of code review, both giving and receiving feedback. In this class, we’ll instead focus on the magic of having a computer check your code for you, which in turn requires doing a good job explaining to the computer what correctness means for each program and why each program is correct. You’ll see that the code comments that pass for that activity in most projects aren’t nearly as detailed and are much more ambiguous than we require for correctness proofs.

Static types

Testing and code reviewing can increase our confidence that a program is correct (and they can give us counterexamples that prove the presence of a bug), but if we would like the computer to do more work for us, static type checking is the very widely used next step.

A type is a set of values along with operations that can be performed on those values.

For example, you are familiar with a variety of types in Python, including:

• int and float, the types of numbers like 42 and 4.2
• str, for character sequences such as "abc", "a", and ""
• bool, the type of True and False

Operations include all the ways we manipulate values of these types, including:

The type signature in the syntax above shows «name of the operation» : «type(s) of inputs» → «type(s) of outputs».

At run-time, the type of a value can determine the behavior of the program. For example:

3.1 + 2.4 # => 5.5

… uses the floating-point addition operation above. But this program:

3.1 + "two point four" # => TypeError: unsupported operand type(s) for +: 'float' and 'str'

… results in a TypeError because + : float × str → ? is not an operation built into Python.

In static type checking, we analyze the types before running the program. To enable this analysis, we have to include type annotations in our program code, explaining which variables have which types. Here is our example with type annotations added:

def indexOf(lst: list[int], elt: int) -> int:
    if lst[0] == elt:
        return 0
    elif len(lst) == 1:
        return -1
    else:
        restidx = indexOf(lst[1:], elt)
        return restidx + 1 if restidx != -1 else -1

With these annotations, a static type checker such as mypy can validate that:

• operations like lst[1:] and len(lst) are indeed operations on list,
• the function indexOf always returns an integer (or raises an error),
• and every place that we call indexOf, it would check that calls always passed two arguments of the appropriate types.

$ mypy indexof.py
Success: no issues found in 1 source file

If we replace the return -1 inside the len(lst) == 1 branch with return None, thinking that None might make sense as a return value in this case, static type checking can identify an inconsistency:

$ mypy indexof.py
indexof.py:5: error: Incompatible return value type (got "None", expected "int")  [return-value]
Found 1 error in 1 file (checked 1 source file)

        restidx = indexOf(lst[1], elt)

Specifications

Unstated in our discussion so far is a conspicuously missing piece: a definition of what indexOf ought to do in order to be considered correct! You might have made some assumptions about what that means, but if we hope to prove it, we cannot rely on assumptions. We must give indexOf a precise specification.

You have plenty of informal experience with specifications from 6.101, written as docstrings:

def indexOf(lst, elt):
    """
    Returns the position of integer element "elt" in a list of integers "lst".
    """
    ...

In this course, the formal specifications are part of the Dafny code, and static checking will encompass proving the validity of those specifications and the correctness of the code that implements them. At this point, we should start working in Dafny. Here is indexOf:

method IndexOf(lst: seq<int>, elt: int) returns (result: int)
{
  if lst[0] == elt {
    return 0;
  } else if |lst| == 1 {
    return -1;
  } else {
    var restidx := IndexOf(lst[1..], elt);
    return if restidx != -1 then restidx + 1 else -1;
  }
}

You can consult Chapter 1 of Program Proofs or read the first part of Dafny’s Getting Started tutorial for an introduction to the basics of the language.

In this example we can spot a few differences from Python:

• the keyword method introduces the declaration; for now, think of it as a synonym for “function”
• curly braces instead of indentation to demarcate blocks
• := instead of = to perform assignments, and semicolons to terminate statements
• the reordered if ... then ... else ... expression instead of Python’s ... if ... else ...
• the mathy notation |lst| instead of len(lst)
• and static types in the declaration!

The specification of this function includes the statically declared types of its inputs and outputs:

• lst: seq<int> specifies that the first argument lst must be a sequence of integers; Dafny sequences are similar to Python tuples (that is, just like Python lists are mutable but Python tuples are immutable [read-only], Dafny provides immutable sequences).
• elt: int specifies that the second argument must be an integer.
• and result: int says that the function will return an integer, and we can refer to that number as result in our specification.

Providing these static types is enough for Dafny to identify, without running the code, a bug that may have been… bugging you… since the beginning of this reading:

$ dafny verify indexof.dfy
indexof.dfy(3,8): Error: index out of range
  |
3 |   if lst[0] == elt {
  |         ^
Dafny program verifier finished with 0 verified, 1 error

Very exciting! The code fails to handle the case where the input lst is empty, and Dafny’s static checking is able to point out the error: index 0 may be out-of-range. (We already saw that mypy was not so clever, and this mistake was not a static error even when we annotated the Python with static types.)

Preconditions

How should we fix the bug? One way we can solve the problem is to add a precondition: a requirement on the inputs to the function, which must be satisfied by the caller:

method IndexOf(lst: seq<int>, elt: int) returns (result: int)
  requires |lst| > 0
{
  // ...

With this specification, it is simply illegal to call indexOf with an empty sequence.

And if we run dafny verify it will report no errors, which means it has proved the program correct! But not for a terribly interesting specification, because indexOf only specifies what the caller must do and says very little about what the implementation must do.

Postconditions

We can make the specification more useful by adding a postcondition: a requirement on the outputs from the function, which must be satisfied by the implementer.

Here are two different specifications for indexOf where we have added postconditions to relate the value of result to the values of lst and elt:

method IndexOf(lst: seq<int>, elt: int) returns (result: int)
  requires |lst| > 0
  ensures result < 0 ==> elt !in lst                           // version (A)
  ensures result >= 0 ==> result < |lst| && lst[result] == elt //            

This specification uses a pair of ensures cases, each of which is stated as an implication with the ==> operator.

method IndexOf(lst: seq<int>, elt: int) returns (result: int)
  requires |lst| > 0
  ensures (result == -1 && elt !in lst)                  // version (B)
          || (0 <= result < |lst| && lst[result] == elt) //            

This specification uses a single ensures structured as a disjunction between two possibilities.

module Version_A {
  method IndexOf(lst: seq<int>, elt: int) returns (result: int)
    requires |lst| > 0
    ensures result < 0 ==> elt !in lst
    ensures result >= 0 ==> result < |lst| && lst[result] == elt
  {
    if lst[0] == elt {
      return 0;
    } else if |lst| == 1 {
      return -1;
    } else {
      var restidx := IndexOf(lst[1..], elt);
      return if restidx != -1 then restidx + 1 else -1;
    }
  }
}

module Version_B {
  method IndexOf(lst: seq<int>, elt: int) returns (result: int)
    requires |lst| > 0
    ensures (result == -1 && elt !in lst)
            || (0 <= result < |lst| && lst[result] == elt)
  {
    if lst[0] == elt {
      return 0;
    } else if |lst| == 1 {
      return -1;
    } else {
      var restidx := IndexOf(lst[1..], elt);
      return if restidx != -1 then restidx + 1 else -1;
    }
  }
}

Invariants

Let’s consider a third way to implement indexOf, perhaps even the way that first comes to mind based on your prior programming experience:

def indexOf(lst, elt):
    for i in range(len(lst)):
        if lst[i] == elt:
            return i
    return -1

Is this code correct? Here it is in Dafny, and the system is not convinced that our code is correct:

method IndexOf(lst: seq<int>, elt: int) returns (result: int)
  requires |lst| > 0
  ensures result < 0 ==> elt !in lst
  ensures result >= 0 ==> result < |lst| && lst[result] == elt
{
  for i := 0 to |lst| {
    if lst[i] == elt {
      return i;
    }
  }
  return -1;
}

As you can see, Dafny is not sure that, if and when we reach return -1, the implication that elt !in lst will definitely hold.

Are you sure that it will hold? Why?

We can formalize our reasoning by stating an invariant: a property that is always true about some values in the program. Here, we have an invariant about the relationship between lst, i, and elt that is established and maintained throughout the execution of the for loop. In English, that invariant is: “elt is not in lst up to index i.”

method IndexOf(lst: seq<int>, elt: int) returns (result: int)
  requires |lst| > 0
  ensures result < 0 ==> elt !in lst
  ensures result >= 0 ==> result < |lst| && lst[result] == elt
{
  for i := 0 to |lst| {
    if lst[i] == elt {
      return i;
    }
  }
  return -1;
}

It’s very reasonable to ask at this point, why did Dafny automatically prove the recursive version and not the loop version? The answer is that it’s impossible to write a program checker that is smart enough to prove all correct programs. The formal concept of undecidable problems from computability theory lets us be precise. We’ll save in-depth treatment of undecidability for other classes, but the upshot for us is that, since full automation is impossible, we often need to give the Dafny checker hints, by translating some of our informal knowledge of a program’s behavior into code. Sometimes a new version of Dafny adds smarter heuristics that increase automation, but the safest strategy is to add enough annotations so that correctness becomes very obvious, even to a “dumb algorithm.” You’ll build your intuition for “obvious” in Dafny as we cover more features and examples, and we will also scratch the surface of explaining how Dafny works internally, which helps predict when automation should succeed.

The goals of 6.S057

Why are we studying program correctness? Well, one timely reason comes from the connection to automatic programming by artificial intelligence. When a strange alien being (e.g., an LLM) writes a long program for you, how do you know it gave you a program that behaves like you want? One great answer is that the alien should also write a machine-checkable proof of correctness! We specialists in the field have been saying “forever” (well, since the 1960s at least) that programming is hard even for humans, and hence formal proof of programs is valuable to catch bugs. Now the mainstream of the tech industry agrees, when we focus on AI as the programmer.

Software-engineering practice is evolving quickly, and, for high-end jobs, it may soon be essential to be able to shepherd through proof of correctness for generated code. Even if not, the habits of mind for this class will help you think clearly about the structure of code, why it is correct, and how to explain to someone else why. Perhaps you’ll find yourself in a job where you write those justifications only in English comments, not formal specifications. If so, you’ll have a leg up in writing clear, unambiguous specifications, having worked with an especially demanding judge, Dafny.

Summary

This reading introduced the notion of correctness with respect to a specification, and we saw our first examples of preconditions, postconditions, and invariants.