Abstract
The main contribution of this paper consists of a description of a front-end tool which supports the computer-aided specification and verification of a class of flowcharts which capture the basic dynamics of object-oriented programs. The specific emphasis of our approach is on the automated verification of flowcharts annotated with assertions which allow one to specify properties directly in terms of the source code itself instead of some particular model of its semantics.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abraham-Mumm, E. and De Boer, F. S. (2000). Proof-outlines for threads in Java. Proceedings of CONCUR 2000, Lecture Notes in Computer Science, Vol. 1877. URL: http://www.cs.princeton.edu/—isabelle/bali/.
De Boer, E S. (1999). A WP-calculus for 00. Proceedings of Foundations of Software Science and Computation Structures (FOSSACS), Lecture Notes in Computer Science, Vol. 1578.
Hatcliff, J. and Dwyer, M. (2001). Using the Bandera tool set to model-check properties of concurrent Java software. Proceedings of CONCUR 2001, Lecture Notes in Computer Science. URL: http://web.clas.ufl.edu/users/rhatch/SAM-V-Z.htm/appel/modernIjava/CUP/.
Huisman, M. (2001). Reasoning about Java programs in higher order logic with PVS and Isabelle. IPA Dissertation Series 2001–03. ISBN 90–9014440–4.
URL: http://www.cl.cam.ac.uk/Research/HVG/HOL/.
URL: http://www.cs.princeton.edu/—appel/modern/java/JLex/.
URL: http://www.cs.kun.nl/—bart/LOOPL
Owre, S., Rushby, J. and Shankar, N. (1992). PVS: A prototype verification system. Proceedings of the 1th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 617.
Poetzsch-Heffter, A. and Mueller, P. (1998). Logical foundations for typed object-oriented languages. Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET98).
Reus, B., Wirsing, M. and Hennicker, R. (2001). A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models.
Proceedings of FASE 2001, Lecture Notes in Computer Science, Vol. 2029.
De Roever, W.-P., De Boer, F. S., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M. and Zwiers, J. (2001). Concurrency Verification. Cambridge University Press.
Warmer, J. B. and Kleppe, A. G. (1998). The object constraint language: precise modeling with UML. Addison-Wesley Object Technology Series.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 IFIP International Federation for Information Processing
About this paper
Cite this paper
de Boer, F.S., Pierik, C. (2002). Computer-Aided Specification and Verification of Annotated Object-Oriented Programs. In: Jacobs, B., Rensink, A. (eds) Formal Methods for Open Object-Based Distributed Systems V. FMOODS 2002. IFIP — The International Federation for Information Processing, vol 81. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35496-5_12
Download citation
DOI: https://doi.org/10.1007/978-0-387-35496-5_12
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-5268-7
Online ISBN: 978-0-387-35496-5
eBook Packages: Springer Book Archive