Dévai, G. 2008. Programming language elements for correctness proofs. Acta Cybernetica. 18, 3 (Jan. 2008), 403-425.