|
|
 |
| |
|
|
|
A Partial Correctness Proof for Programs with Decided Specifications |
|
|
|
PP: 195-202 |
|
|
|
Author(s) |
|
|
|
A. A. Darwish,
|
|
|
|
Abstract |
|
|
| 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. |
|
|
|
|
|
|
|
