|4.13 Interface FS-PVER|
The category of methods PVER - Program Verification serves as proof that a program is an implementation of a formal specification. Input for PVER therefore is a formal specification and depending on the selected individual PVER method possibly a program (this is so for the Classical Program Verification and the Verification during Development (Program Verification)). Depending on the selected individual PVER method the result is a program (this is so for the Formal Transformation (Program)) or an assessment result.
Therefore, FS - Formal Specification is applied for the description of the system, PVER, on the other hand, is applied for the proof that the implementation is consistent with the formal specification.
Therefore, the program has the following pre- and postconditions (specification):
The PASCAL-like program shall be (the greek letters are marking the important places for the proof):
var a, b, c: Integer;
a := 0; b := 1; c := 1;
alfa: while c <= n do beta: a := a+1;
b := b+2;
c := c+b enddo;
PVER now shall prove the partial correctness of the program (if the program terminates, the result meets the specification) and the termination of the program (the program is ending after finite time):
At the beginning of the loop (at alfa:) variable a has the value 0, variable b the value 1 and variable c the value 1. In order to prove the while loop, an invariant is searched, i. e. characteristic that is valid at the beginning of every loop run (at beta:).
The idea for the invariant is:
b= (2*a+1) /\ c = (a+1)2
At the first call of the loop the validity of the invariant obviously is given (because a = 0 and b = c = 1).
If the invariant is true at the beginning of the loop, then it is also valid after (the values of the variables before the loop run are marked by ', e. g. a' for the value of variable a).
Valid after the loop run:
a=a'+1 /\ b=b'+2 /\ c=c'+b
a=a'+1 /\ b=b(2*a'+1)+2 /\ c=(a'+1)2+b according to the reduction requirement
a=a'+1 /\ b=b(2*a+1) /\ c=a2+2*a+1 by logic transformations.
It is obvious that the invariant is also valid after a loop run. It follows from the induction rule that the invariant is valid before every loop run. The assertions follows from the loop termination condition and because a is increased by 1 at every loop run.
The termination may be proved via c: This means c always is a natural number and is really increased at every loop run (cf. invariant). After n+1 loop runs at the latest the program has to terminate because the termination condition c > n is true.PVER tool support is absolutely necessary, the evaluator (respectively the applied rules) has to be adjusted to the selected specification language and the programming language.
|/Baader, 1990/||Basic features of formal methods and a stock-taking of tools and concepts|
|/Brix, 1986/||By means of the examples CARTESIANA a verification tool of Siemens, the basic features of "Program Verification during Development" are explained|
|/Kersten, 1990/||Several reports to "formal specification and verification"|
|/Kröger, 1987/||Deals with temporal logic and verification of statements in temporal logic|
|/Loeckx, 1987/||Describes the mathematical background of several formal verification methods (i. e. Floyd Method, Axiomatic Method of Hoare, Fixed-point Induction), shown by means of some examples. Furthermore the problems of correctness and completeness are discussed|
|GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster|