Comparing Test, Model-checking and Proof

The binary search algorithm

Testing a binary search implementation

In this first part, our goal is to assess the correctness of an implementation of the binary search algorithm in the C language, using software testing.

The C file binsearch1.c contains an implementation of the binary search algorithm.

1. Without looking at the code, compile binsearch1.c with command cc -std=c99 -Wall -O0 -g -o binsearch1 binsearch1.c. Then run several tests to assess the termination and the correctness of this implementation.
2. If some test failed, use a debugger (gdb, lldb,…) to simulate the execution of program binsearch1 and understand the bug.

We propose an alternative implementation of the binary search algorithm in file binsearch2.c. Without looking at the code, compile and test the new implementation. What can you conclude?

Model-checking (a model of) the binary search implementation

In this second part, we use model-checking to check the correctness of a TLA+ model of the binary search algorithm.

1. Verify the TLA+ model of the binary search algorithm in file binsearch1.tla. Fix the model if necessary until you get an algorithm that satisfies the specification. What can you conclude?
2. Proceed similarly with file binsearch2.tla. What can you conclude?

Proving the binary search algorithm

Finally, we assess the correctness of the binary search algorithm using the Dafny prover.

1. What are the loop invariant and variant that must hold for the correctness and termination of the binary search algorithm?
2. Using the loop invariant and variant to prove (informally) that your algorithm is correct.
3. Formally prove the algorithm in file binsearch.dfy using Dafny
4. What can you conclude?

Comparing the three methods

1. Give advantages and drawbacks of the three methods used above. Explain in which context they can be used.

A concurrent program

We consider a program with N processes that share an integer variable x. Each thread first stores the value of x in a local variable y, and then, writes the value of y+1 in x. We expect that the value of x has increased by N when all processes have terminated.

Testing an implementation in the C language

1. Compile the file concurrent_inc.c with the command cc -std=c99 -Wall -o concurrent_inc concurrent_inc.c -lpthread. The resulting executable concurrent_inc takes a number N of processes on the command line, and runs N concurrent processes as described above. Test the program for several values of N. What can you conclude?

Model-checking (a model of) the concurrent algorithm above

1. The file concurrent_inc.tla contains a TLA+ model of the multiprocess program described above as well as a specification. Check if the model staisfies the specification. What can you conclude?