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.

- Define the pre-condition and the post-condition of an algorithm that solves the Dutch national flag problem.
- 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?
- 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?