Invariant Assertions for Program Proofs

There are a few different methods for formally proving that a program agrees with its specifica-tion. The first method we will examine is the invariant assertion method. The method was first proposed for flowcharts by Robert Floyd [3] and then adapted for program code by Tony Hoare [5]. Edsger Dijkstra developed another variant of the method a few years later [1, 2]