A Partial Correctness Proof for Programs with Decided Specifications
Ashraf A. Darwish · 2007
This paper provides the method and complete proof for programs written in Pascal programming language with decided specifications for programs which reverse the digits of an integer from [5]. The author of this paper describes a new concept of partial correctness of programs better suited to specification purposes than the classical one. Partial correctness specifications are pairs of assertions, preconditions and postconditions. As an application of partial correctness specifications, the paper presents the correctness method for some of the programs which have been written in procedural programming language. Moreover, this method is suitable for all procedural programs.