Error-free software:know-how and know-why of program correctness - BABER (Wiley series in software engineering practice, 1991)