Rigorous Methods for Software Construction and Analysis - Abrial, Jean-Raymond; Glässer, Uwe; Kanade, Takeo (Springer Berlin Heidelberg, 2009)