CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Wolfgang Ahrendt (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Frank S. de Boer ; Immo Grabe
A. Cavalcanti and D. Dams, FM 2009: Formal Methods, Second World Congress, Eindhoven (03029743). Vol. 5850 (2009), p. 612 - 627.
[Konferensbidrag, refereegranskat]

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.

Denna post skapades 2009-12-18. Senast ändrad 2016-07-06.
CPL Pubid: 104369


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)



Chalmers infrastruktur