Extended static checking by calculation using the pointfree transform

• Autor(es): Oliveira, José Nuno Fonseca
• Data: 2009
• Identificador Persistente: http://hdl.handle.net/1822/24572
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): Formal methods; Proof obligations; Extended static checking; Theoretical foundations
• Tipo de Documento: Artigo
• Idioma: Inglês

Descrição

The pointfree transform offers to the predicate calculus what the La- place transform offers to the differential/integral calculus: the possibility of chang- ing the underlying mathematical space so as to enable agile algebraic calculation. This paper addresses the foundations of the transform and its application to a calculational approach to extended static checking (ESC) in the context of ab- stract modeling. In particular, a calculus is given whose rules help in breaking the complexity of the proof obligations involved in static checking arguments. The close connection between such calculus and that of weakest pre-conditions makes it possible to use the latter in ESC proof obligation discharge, where point- free notation is again used, this time to calculate with invariant properties to be maintained. A connection with the “everything is a relation” lemma of Alloy is estab- lished, showing how close to each other the pointfree and Alloy notations are. The main advantage of this connection is that of complementing pen-and-paper pointfree calculations with model checking support wherever validating sizable abstract models.