Extended static checking by calculation using the pointfree transform

• Author(s): Oliveira, José Nuno Fonseca
• Date: 2009
• Persistent ID: http://hdl.handle.net/1822/24572
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Formal methods; Proof obligations; Extended static checking; Theoretical foundations
• Document Type: Article
• Language: English

Description

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.