Program verification - Francez, Nissim (Addison-Wesley Pub., 1992)