Program correctness methods and language definition
Edward A. Ashcroft · 1972
The development of the method of proving correctness of programs is considered in relation to methods of defining programming languages. Informal methods are given for checking proposed adaptations of the correctness method to new programming languages. It is shown how correctness-formulae can be considered as semantic definitions of programs, and how Burstall's logical language definitions can be considered as correctness formulae.