The attached code is an implementation of problem 2 in SPARK. However, the code does not follow the algorithm outlined in the problem description and no proof was really attempted because of lack of time to invest into the challenge.
The code is annotated with executable contracts, however, which allowed to find two bugs in the implementation.
language : SPARK 2014
tool : SPARK 2014 (gnatprove)