=ADD=
=reftype=
14
=number=
98-02a
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1998/98-02a.ps.gz
=year=
1998
=month=
03
=author=
Rolletschek; Heinrich
=title=
Formal Specification and Verification (Lecture Notes)
=abstract=
   In these lecture notes the basic theory of program verification is introduced.
   In an introductory chapter the fundamental concepts (specification, partial
   and total correctness) are defined. Chapter 1 deals with the basic proof rules,
   which allow to handle conditionals, while-loops and other control structures.
   In chapter 2 these rules are put on a rigorous mathematical basis, using a
   formal definition of the semantics of a programming language; this chapter also
   presents the theory of weakest pre- and strongest postconditions. Chapter 3
   briefly deals with a mixture of topics which are summarized under the headline
   `Applications of program verification.' On the one hand, it is shown how
   verification could be carried out for programs executed on a real rather than
   idealized (mathematical) computer, and on the other hand, an application of
   the verification methods for the purpose of complexity analysis is given. The
   last two chapters, finally, show how to verify programs containing structured
   data types and subroutines, respectively.
=keywords=
specification, verification
=end=