Verifying the binary search algorithm

Testing a binary search implementation

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

  1. Without looking at the code, compile binsearch.c with command cc -std=c99 -Wall -O0 -g -o binsearch binsearch.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 binsearch 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

  1. Model the binary search algorithm implemented in binsearch.c with PlusCal.
  2. Add a specification and check the termination and the correctness of the algorithm. Fix the model is necessary until you get an algorithm that satisfies the specification. What can you conclude?
  3. Proceed similarly with file binsearch2.c. What can you conclude?

Proving the binary search algorithm

  1. What are the loop invariant and variant that must hold for the correctness and termination of your binary search algorithm?
  2. Using the loop invariant and variant to prove (informally) that your algorithm is correct.
  3. Formally prove your algorithm using Dafny binsearch.dfy
  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.