AssertionTypes
Full Title
Assertion Types for Object-Oriented ProgrammingDescription
The project investigates the problem of designing an assertion language for an object-oriented language that allows for expressing properties of, and reasoning about, objects and their invariants. The programming language should be rich enough to encompass common features expected in modern, flexible programming languages, such as state, dynamic object creation, reference-passing and aliasing, and thread creation. The assertion language should be able to talk about objects at different levels of detail, ranging from interface types, to deep properties of objects. Annotations vary in precision, from conventional interfaces describing input-output, through more expressive yet still decidable invariants of components, to detailed properties expressing for example, object invariants, and, in the case of multiple threads, progress and absence of races when accessing shared resources.