The foundations of program verification - Loeckx, Jacques (Wiley-Teubner Series in Computer Science, 1987)