In "Related Work", a reference is missing to the annotation method of Deransart for proving program correctness [Deransart and Małuszyński 1993, Deransart 1993, Boye and Małuszyński 1997]. As briefly described in [Drabent and Miłkowska 2005, Section 5]:
An approach related to ours is the annotation method of Deransart [Deransart 1993, section 4; Boye and Małuszyński 1997, section 4] for proving definite program correctness. It can be seen as refinement of the natural method of section 3.1, where one proves more (but smaller) implications than those to be proved in the natural method.Here "natural method" stands for the method of Theorem 4.1 by Clark . It is worth adding that the attribution of the method to Clark is due to Deransart .