The Dutch national flag problem

The Dutch national flag problem is a partitioning problem proposed and solved by E. Dijkstra in the 1970s. A description of the problem can be found on Wikipedia. The algorithms takes as inputs an array t with domain 1..N and values in 0..MAXINT (N and MAXINT are parameters), and two values low and high in 0..MAXINT, such that low < high. The value low represents the biggest "red" value and high is the smallest "blue" value.

  1. Define the pre-condition and the post-condition of an algorithm that solves the Dutch national flag problem.
  2. Write a PlusCal algorithm that solves the problem and prove that your algorithm satisfies the specification using the TLA toolbox. What can you deduce of the verification results?
  3. What are the loop invariants needed to prove the correctness of your algorithm? How can you check that these invariants hold on the executions of the algorithm?