/* 1. Write a function that checks if an array of a given length is
* sorted.
*/
/* 2. Write a function that creates an array of a given length
* containing non-deterministic values.
*/
/* 3. Write a sort function for an array of a given length.
*/
/* 4. Using the code from 1. and 2. create a verification harness and
* prove that the output of the sort function is actually sorted.
*/
/* 5. Is the output of 4. sufficient to prove the sort function
* correct?
*/