TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs

Radu Grigore, Rasmus Lerchedahl Petersen and Dino Distefano

Abstract

In this paper we present ongoing work related to a new specification language for temporal safety properties aimed at object-oriented software. The language is expressive enough to represent relationships between objects and it is designed with the goal of performing both dynamic and static analysis. We present the formal semantics and discuss dynamic checking with respect to a simple object-oriented language.

Full paper

Slides

o

Presented at FOOL 2011; Sunday, 23 October 2011; Portland, Oregon, USA