CW 324

J. Dockx, M. van Dooren, E. Steegmans
Different implementations in Java of a nested loop and their proofs

Abstract

In this technical report, we prove the correctness of different implementations of a given specification. This way, we show that using internal iterators dramat ically shortens the length of a proof of correctness, and thus the complexity of the code. A remarkable outcome is that introducing a helper method no longer sh ortens the proof when internal iterators are used, but makes it longer.