Abstract
In this paper we give a representation of a weakest precondition calculus for abstract object creation in dynamic logic, the logic underlying the KeY theorem prover. This representation allows to both specify and verify properties of objects at the abstraction level of the (object-oriented) programming language. Objects which are not (yet) created never play any role, neither in the specification nor in the verification of properties. Further, we show how to symbolically execute abstract object creation. © 2009 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Ahrendt, W., De Boer, F. S., & Grabe, I. (2009). Abstract object creation in dynamic logic to be or not to be created. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5850 LNCS, pp. 612–627). https://doi.org/10.1007/978-3-642-05089-3_39
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
