This Article 
 Bibliographic References 
 Add to: 
On the Development of Correct Specified Programs
September 1981 (vol. 7 no. 5)
pp. 519-527
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.
Index Terms:
sorting, Assertion-specified programs, bubblesort procedures, program correctness, program development, PROMET-1
A.J. Blikle, "On the Development of Correct Specified Programs," IEEE Transactions on Software Engineering, vol. 7, no. 5, pp. 519-527, Sept. 1981, doi:10.1109/TSE.1981.231114
Usage of this product signifies your acceptance of the Terms of Use.