ASSERTION-TYPES for Object-Oriented Programming

Period: 
January 2010 to June 2012
Funded by: 
FCT (PTDC/EIA-CCO/105359/2008)
External Members: 

Marco Giunti

Tiago Santos

Description: 

The construction of reliable software is an extremely difficult endeavour. For large systems it requires modular development strategies, that are ideally founded on precise and trusted interface specifications. In practice, however, programmers work with a large collection of APIs whose behaviour is only informally and imprecisely specified. Practical mechanisms for specifying and verifying precise, behavioural aspects of interfaces are in clear need.
In this project we will develop flexible source level program analysis tools to support gradual reasoning about programs, by building on dependent-type or type-effect systems, decidable fragments of logics, constraint solving, and even general theorem proving. Static type systems have proved to be extremely effective and practical tools to check basic interface properties of modules, and are adopted by many large software development projects. However these systems are somewhat limited in the kind of properties they can express, seldom going beyond the input-output behavior of modules.
On a different strand, current software development practice is frequently based on dynamic languages that allow to quickly express concepts, prototype ideas, get the architecture clear and visible, and then fill it out to produce an application. Then, as the application gets larger or when the code is to be turned into an API to be shared by multiple clients, the need for modularity arises and developers have no choice but to rewrite their applications in a different, statically typed, language.
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.
The compiler that will be built checks programs against specifications and generates safe code. Towards this end we will take advantage of the combination of several mechanisms, including constraint and Damas-Milner inference, type checking, and the employment of proof assistants. Assertions that fail to be statically checked are transformed into run-time checks within the generated code. To help the swift development of applications, we envisage a system where the sought properties of programs can be gradually added, and where the different trade-offs between static and dynamic checks can be easily chosen by the developer, thus forgoing the need to change programming language when a quickly prototyped application comes to require more comprehensive guarantees.
Research on assertion languages, in the form of contracts and dependent/refinement types, have so far concentrated mostly on functional languages. We believe our approach will make the difference in a flexible software development process using mainstream programming languages, with a controlled degree of static checks, while always ensuring safe run-time code. Our compiler, when run in a fast interactive mode, performs only limited static analysis to detect obvious type errors, while in production mode it may perform deeper analysis to detect more defects statically and generate improved code with less dynamic checks.
We expect to produce an hybrid compiler for an object-oriented programming language with an expressive specification language where envisaged properties of programs can be gradually added, and where the different trade-offs between static and dynamic checks can be easily chosen by the developer. A notable characteristic of the compiler is the exploitation of a theorem prover while trying to prove non-decidable assertions. We will also deliver studies on the software development process under the proposed methodology for several case studies on common object-oriented patterns.