On correct program development
Andrzej Blikle · International Conference on Software Engineering · 1979
The paper presents a method of correct programs' derivation. Our programs consist of an operational part (the virtual program) and a specification. Both these parts are subject to the development and the refinement process. Specifications consist of a precondition and a postcondition (global specification) plus a set of assertions (local specification). A program is correct if: l) it is partially correct wrt the global specification, 2) the precondition guarantees that the program neither loops indefinitely nor aborts, 3) the assertions are adequate for the proof of l) and 2). Programs are developed by means of correctness preserving transformations. The requirement of handling the problem of abortion leads to the necessity of using a partial (or three valued) logic, We are using McCarthy's logic for this purpose.