Programming from Specifications (Prentice Hall, 1990)