William A. Wulf, Ralph L. London, Mary Shaw: An Introduction to the Construction and Verification of Alphard Programs. IEEE Trans. Software Eng. 2(4): 253-265 (1976)