Verifying a Class: combining Testing and Proving

• Autorzy: Mirkowska G. , Salwicki A. , Świda O.
• Języki publikacji: EN

Abstrakty

EN

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 AC 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.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 95, nr 2/3
• Strony: 303--324
• Opis fizyczny: Bibliogr. 9 poz., tab., wykr.

Twórcy

autor

Mirkowska G.

autor

Salwicki A.

autor

Świda O.

• Faculty of Mathematics and Natural Sciences, University Cardinal Stefan Wyszyński, Wóycickiego 1/3, 01-938 Warszawa, Poland,

Bibliografia

• [1] Amey, P.: Logic versus Magic in Critical Systems, Reliable Software Technologies - Ada Europe 2001, Lecture Motes in Computer Science 2043, Springer, 2001.
• [2] Barnes, J.: High Integrity Software, Addison-Wesley, London, 2003.
• [3] Meyer, B.: Object-Oriented Software Construction (Eiffel), Prentice Hall, 1997.
• [4] Mirkowska, G., Salwicki, A.: Algorithmic Logic, PWN and J.Reidel, Warszawa, 1987.
• [5] Mirkowska, G., Salwicki, A., ´Swida, O.: SpecVer - the methodology integrating specification, programming and verification, Fundamenta Informaticae, 85, 2008, 343-357.
• [6] Ratajczak-Bartol, W., Szczepańska-Wasersztrum, D.: Data Structure for Simulation Purpose in Loglan77, Technical Report 373, Institute of Computer Science, Polish Academy of Sciences, Warszawa, 1979.
• [7] Ratajczak-Bartol, W., Szczepańska-Wasersztrum, D.: Code of Simulation and other Classes, http://duch.mimuw.edu.pl/~salwicki/EOP/PQclass.html, October 2007.
• [8] Salwicki, A.: On Algorithmic theory of Stacks, Fundamenta Informaticae, 3, 1980, 311-332.
• [9] Świda, O.: SpecVer - Specification, Verification, Programming, a plugin into Eclipse, http://aragorn.pb.bialystok.pl/~swida/svp, April 2007.