@inbook {Ol08b ,
	title = {Extended Static Checking by Calculation using the Pointfree Transform},
	booktitle = {LerNet ALFA Summer School},
	volume = {5520},
	year = {2009},
	pages = {195{\textendash}251},
	publisher = {Springer-Verlag},
	organization = {Springer-Verlag},
	abstract = {<p>The pointfree transform offers to the predicate calculus what the Laplace transform offers to the differential/integral calculus: the possibility of changing 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 abstract 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 pointfree notation is again used, this time to calculate with invariant properties to be maintained. A connection with the {\textquotedblleft}everything is a relation{\textquotedblright} lemma of Alloy is established, 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.</p>
},
	doi = {10.1007/978-3-642-03153-3_5},
	author = {Jos{\'e} Nuno Oliveira}
}