On software verification

In order to rely with confidence upon any particular program, it is not sufficient to know that the program works most of the time or even that it has never made a mistake so far. The real question is whether it can be counted upon to fulfill its functional specifications successfully every single time. This means that, after a program has passed the checkout stage, there should be no possibility that an unusual combination of input data or conditions may bring to light an unexpected mistake in the program. Every portion of the program must be utilized during checkout in order that its correctness may be confirmed.

― Joan C. Miller and Clifford J. Maloney, Systematic Mistake Analysis of Digital Computer Programs, ACM, 1963.

Our approach to software testing hasn’t changed much since the introduction of software verification in the 1950s or 1960s. We have come up with tools and automation, but the process has essentially remained the same. This is no surprise, because our goal hasn’t changed either: ensuring the correctness of the software we write.

Consider the following piece of Rust code, for example:

type Coord = i32;

struct Point {
    x: Coord,
    y: Coord
}

#[allow(non_snake_case)]
struct Triangle {
    A: Point,
    B: Point,
    C: Point
}

#[allow(non_snake_case)]
impl Triangle {
    fn dist2(p: &Point, q: &Point) -> i128 {
        let dx = (p.x as i128) - (q.x as i128);
        let dy = (p.y as i128) - (q.y as i128);
        dx * dx + dy * dy
    }

    pub fn is_right_at_C(&self) -> bool {
        Triangle::dist2(&self.A, &self.B)
            == Triangle::dist2(&self.B, &self.C) + Triangle::dist2(&self.C, &self.A)
    }
}

It implements two structs that describe a triangle on a plane, as well as two functions that verify whether the triangle has a right angle at $C$ .

The function is_right_at_C is supposed to return true if $C = \pi/2$ . It does this by verifying the following identity:

c^2 = a^2 + b^2

Alternatively, we could have checked that the dot product of the vectors defining the two legs is $\langle \mathbf{a}, \mathbf{b} \rangle = 0$ .

What is the process for testing this software?

The first level of verification involves comparing the software to its specifications. Does the software do what it is supposed to do?

As the above article by Miller and Maloney summarizes, we should go beyond a simple inspection to cover as many use scenarios and unusual inputs as possible. This is usually achieved through unit testing. Unit tests provide more structured and systematic verification, and prevent unintended modifications, or regressions, as the software evolves.

Unit tests compare the code’s output against the expected output for known inputs (test vectors). For example, the following code snippet verifies that the function is_right_at_C returns true for triangles that we know are right triangles, such as the triple $(3, 4, 5)$ .

#[cfg(test)]
mod test {
    use super::*;

    #[allow(non_snake_case)]
    fn t(Ax: Coord, Ay: Coord, Bx: Coord, By: Coord, Cx: Coord, Cy: Coord) -> Triangle {
        Triangle {
            A: Point { x: Ax, y: Ay },
            B: Point { x: Bx, y: By },
            C: Point { x: Cx, y: Cy }
        }
    }

    #[test]
    #[allow(non_snake_case)]
    fn right_angle_at_C() {
        assert!(t(3, 0, 0, 4, 0, 0).is_right_at_C()); // 3-4-5 triangle
        assert!(t(4, 1, 1, 5, 1, 1).is_right_at_C()); // 3-4-5 triangle, translated
        assert!(!t(1, 0, 1, 1, 0, 0).is_right_at_C()); // not a right triangle
    }

    // check overflow
    #[test]
    #[allow(non_snake_case)]
    fn extremes_do_not_overflow() {
        let (hi, lo) = (Coord::MAX, Coord::MIN);
        let _ = t(hi, hi, lo, lo, hi, lo).is_right_at_C();
        let _ = t(hi, lo, lo, hi, 0, 0).is_right_at_C();
        let _ = t(lo, lo, hi, hi, 0, 0).is_right_at_C();
    }
}

We have historically used two metrics of success: first, that the tests are green, meaning they pass; and second, coverage, which is a measure of how many lines of code were executed while running the tests (more critical in interpreted languages like Python).

Limitations of unit-testing

Although unit tests are useful and necessary, and writing them carefully is somewhat of an art form, they don’t rule out the existence of bugs. We may find a bug or a regression if we’re lucky, but green tests do not guarantee the software is correct. This is just a fact of life.

Program testing can be used to show the presence of bugs, but never to show their absence!

― Edsger W. Dijkstra

Essentially, this boils down to tests not being exhaustive or complete. For example, in the Rust code above, we took some precautions, such as casting the intermediate multiplications to 128 bits to prevent overflow (we could also use big-int arithmetic). If we change the type from Coord = i32 to Coord = i64, for example, one of the tests will fail.

However, these tests are far from exhaustive, and the fact that they pass does not imply that the software is bug-free.

To get that guarantee, we need to ask a different question. Does the code return the correct answer for any triangle defined by integer coordinate points ranging between $-2^{31}$ and $2^{31}-1$ ? How can we be sure that our function is a perfect discriminator and that there are no counterexamples?

In most cases, we can only obtain this guarantee from mathematics, not from testing, because it is impossible to enumerate all examples.

How can we be sure that this code is correct?

Asking this question about the absolute validity of our code brings us into the realm of mathematics.

I know this is a contrived example. I chose it because we know that the relationship tested by the is_right_at_C function is true for any right triangle over $\mathbb{R}$ .

A graphical proof of Pythagoras Theorem. Taken from Yo Yo Math with the gratious permission of the author.

The lengths of the sides in our example are real numbers, so we can conclude that our code is correct $\blacksquare$

But can we get similar guarantees for any software we write?

Software verification with Lean

Most of the time, our software doesn’t resemble a famous theorem. So, how do we get these correctness guarantees?

We express the parts of our software that we want to verify as a theorem and then prove or disprove it. This sounds obvious, right? This can be done using pen and paper, or a proof assistant like Lean.

Lean is both a theorem prover and a functional programming language. First, we write a representation of our code in Lean. Then, we write the statements or theorems about our code that we want to verify. The following diagram describes the process:

Software verification with Rust and Lean

The validity of the entire process depends on how accurately we can translate our model into Lean. The model can be extracted manually or via automatic tools. Strategies such as differential random testing can be used to validate the process.

Returning to our Rust code above: Imagine that we don’t know the proof of the Pythagorean Theorem.

How can we prove that our software is correct for all possible inputs and that the function is_right_at_C will only return true for all right triangles, and only for right triangles?

We can create a Lean model of our code and prove that the relationship we wrote holds for any right triangle.

Proving that our triangle example is correct

The full proof can be opened in interactive mode here:

Open in Lean-Web

In this case, the model is simple enough to be hand-crafted.

Essentially, we are proving the cosine theorem over $\mathbb{Z}$ :

c^2 = a^2 + b^2 - \underbrace{2ab\cos C}_{\text{excess}}

And then that the triangle is right at $C$ if and only if the excess is $0$ , which is Pythagoras theorem.