4.32 Method Cathegory "Program Verification" (PVER) 
4.32 Methodenkategorie "Programmverifikation" (PVER)
Within the Program Verification it is proved by means of formal logic that a program is a refinement of a specification and that all requirements to this higherlevel specification are met too.
The objective of PVER is to mathematically exactly prove that the program code is a correct implementation of the specification.
Means of Representation
On the part of the specification the means of representation described at FS  Formal Specification are applied. On the part of the program a programming language is used. The semantics of the programming language has to be formally defined. Further rules have to be described for the proof steps (e. g. Hoare Calculus).
Operational Sequence
There are three different procedures to do the formal Program Verification, such as to do the formal DVER  Design Verification:
In generally, fully automatic Program Verification is not possible. The verification conditions should be generated automatically. But often, automatically generated verification conditions are very long and therefore are difficult to prove by hand. Tool support therefore is strongly required.
Performing Program Verification requires a sound mathematical education. For those parts of the proof not fully automated (e. g. finding the invariant) much experience is necessary. The program either should be written by the team that shall perform the proof or at least should be written in a form supporting the verification (e. g. invariant recorded in form of comments).
By observing these limitations the IT system development has an enormous chance to generate first rate, highquality IT systems, however, by applying the formal methods.
No.  Activity  Description 

4.1 
SD6.1 Coding of SW Modules, 
The correspondence of the program code to the formal specification used as programming specification is evaluated.

No.  Interface  Observation  Information in Annex 1 

5.1  PVERFS  PVER requires a calculus which describes the semantics of the programming language by means of a specification language (FS).  4.13 Interface FSPVER 
GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster 