# 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.

- 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.
- 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.

- 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?
- 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.

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

### Comparing the three methods

- 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

- 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

- 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?