Abstract Object Creation in Dynamic Logic - To Be or Not To Be Created

No table of content available

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

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

Publikations- och innehållstyp

kon (ämneskategori)

ref (ämneskategori)