Refinement Algebra for an Object-oriented Language with Pointers, 13 Apr 2015


By Prof. Augusto SampaioUniversidade Federal de Pernambuco (UFPE), Brazil

Abstract. A set of laws that captures general properties of (and the relationship among) programming constructs is usually called a “refinement algebra”; when the purpose of the laws is to derive executable programs from specifications, then they are collectively denoted as a refinement calculus. The algebraic style is useful not only to define formal semantics, but also to reason about programs and to serve as a powerful design tool. Several paradigms (imperative, object-oriented, functional, logical, concurrent,...) have benefitted from algebraic programming laws. Also, interesting applications have been designed entirely based on the algebraic style: hardware-software partitioning algorithms, compilers for object-oriented languages and sound refactoring transformations, among others. This talk briefly summarises these advances and addresses our current efforts on a complete set of laws and sound refactoring for an object- oriented language with pointers. Data refinement for class hierarchies is also addressed.

Keywords. Algebraic laws; program transformation; data refinement of class hierarchies.

A Short Bio. Prof. Augusto Sampaio is a graduate of UFPE (1985 and 1988) and Oxford (DPhil, 1993). Currently, Prof. Sampaio is a software engineering professor at UFPE. Linking theories and tools, model and program analysis and transformation, and model based testing are among his major research interests. He has also focused on cooperation with industry: particularly, since 2002 with Motorola, on formal testing and analysis of mobile phone applications; and since 2006 with Embraer, on qualitative and quantitative analysis of models of avionics applications, as well as model based testing.

Coffee session: at 1:30 PM, Sala de Estar, 4th Floor

Talks session: at 2:00 PM, Auditório A2, 1st Floor