Colloquium Series - Summer 1998

By - Mark Utting

Object-oriented systems are typically structured as complex networks of interacting mutable objects. To reason about such systems, simple and efficient techniques for coping with aliasing are needed. In this talk, I describe the important issues that must be addressed for practical reasoning about aliasing, then present a simple solution and its application to C++. I describe its disadvantages (pointer operations must be written in a slightly different style) as well as its advantages (easy reasoning about aliasing, and a useful debugging tool for catching pointer errors).

By - Harish Karnick

We describe a model theoretic (mainly possible worlds) approach to several commonsense reasoning methods like: default reasoning, counterfactual reasoning, autoepistemic reasoning, and probabilistic reasoning. This gives conditions under which a format (theorem) can be said to follow from a theory. We also distinguish between monotonicity/nonmonotonicity of the logic from that of the conditional and discuss whether properties like transitivity, contraposition, modus tollens etc. hold for the conditional.

By- Peter Mueller

Formal specification and verification of object-oriented programs require a strong connection between the programming language, the specification framework, and the verification logic. Specification techniques have to be integrated with their underlying programming languages to be able to handle object structures with aliasing and destructive updates in an expressive and semantically clear way. To have a precise notion of correctness, interface specifications have to be linked formally to proof obligations of the programming logic. This talk presents an integrated specification and verification technique that is capable of the typical object-oriented language features such as object structures with aliasing and side effects, sub-typing, and dynamic binding. We use a formalization of the data and state model of the underlying programming language to provide a formal foundation for interface specifications. The formal meaning of method specifications and class invariants is defined by transforming them into triples of a Hoare-style programming logic. Furthermore, we show how side-effects can be handled by such programming logics.