Towards a Local and Modular Program Logic for Objects

There are many application domains where software failures are not an option. Formal methods allow certain properties of systems to be guaranteed: safety, security and even correctness. Depending on the property of interest, verifying a system can be fully automatic, e.g. when using type systems or model checking; or it can be a tedious manual process, as in the case of deductive verification. Still deductive verification plays an important role in the development of dependable software systems, since it can guarantee program correctness, it is not restricted to finite-state systems and can handle unrestricted programs with rich data structures.

The foundations of deductive verification were set a long time ago by C.A.R. Hoare and his program logic. However, recently we have seen renewed interest in program correctness, both from the industry and academia. In the industry much effort has gone into making full automation possible, at the cost of giving up soundness and completeness of the analysis (JML, ESC/Java or Spec#).

In the research community the direction has been towards program logics that allow local and modular reasoning in the presence of realistic memory models. However, soundness of a logic has to be proved with respect to a semantic model, which clearly separates logical validity from derivability. And in this setting finding good semantic models in which one can reason about the behaviour of programs is challenging.

This is even more challenging in the presence of memory models which allow dynamic storage of executable code. Still, this feature is present in different forms in almost all practical programming languages: pointers to functions in C/C++, callbacks in Java or general references in ML. Classical denotational models based on partial orders are highly complex in this setting, and in the existing ones many equivalences involving state still do not hold.

Step-Indexed Semantical Models of Object Types

An alternative is to use step-indexed semantical models, an approach first introduced by Andrew Appel and his collaborators in the context of foundational proof-carrying code. Their goal was to produce modular machine-checkable proofs of type safety for complex low-level languages. The technique was also applied to a lambda calculus with recursive types, and later successfully extended by Amal Ahmed to general references and impredicative polymorphism.

Based on a small-step operational semantics, types are interpreted as sets of indexed values. Informally, an expression has a certain type if it behaves like an element of that type for a fixed number of steps. As in a denotational semantics types have a meaning: they can be viewed as predicates over programs. However, the model is purely set-theoretic, so much simpler than the models one usually has with a denotational semantics. Type safety is an immediate consequence of this interpretation of types, while the usual type inference rules are proved as independent lemmas, usually by direct induction on the index.

For my Master’s thesis I developed step-indexed semantical models of types for the functional and imperative object calculi. The calculi of Martin Abadi and Luca Cardelli capture the essence of object-oriented programming languages, in the same way Church’s lambda calculus captures the essence of functional programming. And even though objects are the only primitive, they are expressive enough to encode all common features of practical object-oriented programming languages like classes and inheritance.

I investigated the variants of the functional and the imperative object calculi with subtyping, recursive types and polymorphism. The imperative object calculus is a particularly interesting subject of research, since it combines objects with dynamically allocated, higher-order store. And while my model heavily relies on previous results of Amal Ahmed and others, it provides several new contributions: object types, subtyping, bounded quantification and self types.

Towards a Local and Modular Program Logic for Objects

Abadi and Leino extended a very simple type system for imperative objects with first-order logic formulas about the store, producing a logic of objects. This logic is not local, not modular, and it does not support polymorphic or recursive types. The denotational semantical model for this logic was developed by my advisor, Jan Schwinghammer. This model allowed him to prove soundness of the logic, and to extend it to recursive specifications. Still, the model is not abstract enough to capture many natural equivalences involving state, and does not have an elegant treatment of subtyping.

One interesting topic for future research would be to develop a new program logic for the imperative object calculus, by adding dependent types to the strong type system we already considered. Step-indexing could once again be helpful when building the corresponding semantic model. A shallow embedding into higher-order logic similar to the one for the Hoare Type Theory of Aleksandar Nanevski and his collaborators could also help.

This logic should allow local reasoning about the store, in the sense of the separation logic of Peter O’Hearn and John Reynolds. The first separation logic for higher-order store was recently proposed by Bernhard Reus and Jan Schwinghammer, for a very simple While language, so objects would be a big step forward. Finally, it will be great if our logic of objects allows modular reasoning about abstract data structures, similarly to John Reynolds’s specification logic, and the recent results of Neelakantan Krishnaswami on a separation logic for Idealized ML.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: