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.

We consider first-order specifications together with the restriction to accept only programmable algebras as models. We provide a criterion which links this approach with the "generation principle": all programmable models of any specification SP that meets this criterion are reachable. We also show an example of a specification which does not satisfy the criterion and admits a programmable yet nonreachable model. Moreover, a general method of showing the existence of programmable but nonreachable models for a class of first-order specifications is given.

It is commonly believed that a programmable model satisfying the axioms of a given algebraic specification guarantees good properties and is a correct implementation of the specification. This convinction might be related to the Tennenbaum's property

Propositional algorithmic logic PAL is a propositional counterpart of algorithmic logics. It investigates properties of program connectives: begin...end, while...do, if..then..else, or .... PAL supplies tools for reasoning about programs constructed from program variables by means of program connectives and about their algorithmic properties. Sound rules of inference and tautologies of PAL are as important in analysis of programs (e.g. verification) as tautologies of classical propositional calculus. On the other hand propositional algorithmic theories are of highest interest, since they can capture properties of data structures and also algorithmic properties of behaviours of concurrent systems.