Formal Methods Hype

Formal methods build a beautiful hype that software can be verified to be correct given formal specifications and formal execution models that check if the implementation satisfies all the required constraints. A example of the math function abs() is shown below.

	public class AbsTest {
	public static int absSpec(int x) {
	return x < 0 ? -x : x;
	}
	public static int absImpl(int x) {
	int signbits = x >> 31;
	int xor = x ^ signbits;
	return xor + (signbits & 0x01);
	}
	public static void main(String []args) {
	for(int i = -3; i < 5; i++)
	System.out.printf("abs(%d): %s\n",
	i, absImpl(i) == absSpec(i) ? "passed" : "failed");
	}
	}

view raw AbsTest.java hosted with ❤ by GitHub

The absImpl() is a particular implementation and absSpec() specifies the expected output of absImpl(). A formal method verifier such as Dafny is able to check if both outputs are the same. In this example, the specification absSpec() is so convincing that the implementer is confident that the absImpl() is correct. In contrast, what about very complex specifications such as FFT? Unfortunately, the given formal specifications are only supposed to be correct, not necessarily flawless by nature. The correctness simply means the consistency between the implementation and the constraints imposed by the specifications. Whether the formal specifications are correct and address all the informal requirements is a question. The fact turns out developers test the specifications against their implementations. That implies the true correctness of software is still grounded on testing, not on formal verification.