G. Dévai, “Programming language elements for correctness proofs”, Acta Cybern, vol. 18, no. 3, pp. 403-425, Jan. 2008.