Issue No. 05 - September (1981 vol. 7)
A.J. Blikle , Institute of Computer Science, Polish Academy of Sciences
The paper describes a method of program development which guarantees correctness. Our programs consist of an operational part, called instruction, and a specification. Both these parts are subject to the development and the refinement process. The specification consists of a pre-and postcondition called global specification and a set of assertions called local specification. A specified program is called correct if: 1) the operational part is totally correct w.r.t. the pre-and postcondition, 2) the precondition guarantees nonabortion, 3) local assertions are adequate for the proof of 1) and 2). The requirement of nonabortion leads to the use of a three-valued predicate calculus. We use McCarthy's calculus in that place. The paper contains a description of an experimental programming language PROMET-1 designed for our style of programming. The method is illustrated by the derivation of a bubblesort procedure.
sorting, Assertion-specified programs, bubblesort procedures, program correctness, program development, PROMET-1
A. Blikle, "On the Development of Correct Specified Programs," in IEEE Transactions on Software Engineering, vol. 7, no. , pp. 519-527, 1981.