Reasoning about Java classes
- 1 October 1998
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 33 (10) , 329-340
- https://doi.org/10.1145/286936.286973
Abstract
We present the first results of a project called LOOP, on formal methods for the object-oriented language Java. It aims at verification of program properties, with support of modern tools. We use our own front-end tool (which is still partly under construction) for translating Java classes into higher order logic, and a back-end theorem prover (namely PVS, developed at SRI) for reasoning. In several examples we demonstrate how non-trivial properties of Java programs and classes can be proven following this two-step approach.Keywords
This publication has 7 references indexed in Scilit:
- Universal coalgebra: a theory of systemsTheoretical Computer Science, 2000
- Objective ML: An effective object-oriented extension to MLTheory and Practice of Object Systems, 1998
- An approach to object semantics based on terminal co-algebrasMathematical Structures in Computer Science, 1995
- Formal verification for fault-tolerant architectures: prolegomena to the design of PVSIEEE Transactions on Software Engineering, 1995
- Ten Years of Hoare's Logic: A Survey—Part IACM Transactions on Programming Languages and Systems, 1981
- The Science of ProgrammingPublished by Springer Nature ,1981
- An axiomatic basis for computer programmingCommunications of the ACM, 1969