Sorted - Verifying the Problem of the Dutch National Flag in Agda

Abstract

The problem of the Dutch national flag was formulated by Dijkstra (1976) as follows: There is a row of buckets numbered from 1 to n. It is given that : P1 : each bucket contains one pebble P2 : each pebble is either red, white, or blue . A minicomputer is placed in front of this row of buckets and has to be programmed in such a way that it will rearrange (if necessary) the pebbles in the order of the Dutch national flag . The minicomputer in question should perform this rearrangement using two commands: • swap i j for 1≤ i ≤ n and 1≤ j ≤ n exchanges the pebbles stored in the buckets numbered i and j ; • read ( i ) for 1≤ i ≤ n returns the colour of the pebble currently lying in bucket number i . Dijkstra originally named this operation buck .