Niner since 2010
Can the system handle overflow (e.g. if the array of cubes is so large that the cubes of higher indices exceed the maximum integer value)?
Very nice, but I'd like to see the full postcondition for NextChunk. Perhaps, in your next episode, you could give an example of a postcondition containing, say, a quantified expression.