TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs
Radu Gheorghe Grigore · 2011
In this paper we present ongoing work related to a new specification language for temporal safety properties aimed at object-oriented software. The language naturally captures relationships between objects and it is designed with the goal of performing dynamic and static analysis. We present its formal semantics as well as several examples showing its expressivity.