Affiliations: Faculty of Mathematics and Natural Sciences,
University Cardinal Stefan Wyszyński Wóycickiego 1/3,
01-938 Warszawa, Poland. E-mail: [email protected] | National Institute of Telecomunication, Szachowa 1,
04-894 Warszawa, Poland and Faculty of Mathematics and Natural Sciences,
University Cardinal Stefan Wyszyński Wóycickiego 1/3,
01-938 Warszawa, Poland. E-mail: [email protected] | Białystok University of Technology, Department of
Computer Science Wiejska 45A, 15-351 Białystok, Poland.
E-mail: [email protected]
Abstract: The problem of correctness of a class C w.r.t. a specification S is
discussed. A formal counterpart of the problem is the question well known in
metamathematics, whether an algebraic structure is a model of a given theory.
Now, this metamathematical problem has to be adapted to the context of software
engineering. As a theory we consider the (algorithmic) specification S. The
algebraic structure A_C induced by the class C is our candidate for a model of
S. Remark, that this problem differs from the correctness' problem
of an algorithm w.r.t. a pre- and a post-conditions. In the paper we consider
the specification ATPQ of priority queues and the class PQS, and we verify the
correctness of this class with respect to the specification ATPQ. Programmers and software companies prefer to test software instead of proving it. Surely,
proving is more difficult, testing is easier. In this article we combine these
two approaches. Hence, the following actions appear in our method of
verification: experiment, observe, formulate hypotheses, prove. It is our hope
that this method is of general use and adapts well to many practical cases of
verification of object-oriented software.
