@techreport{NordioCalcagnoMuellerMeyer09, author = {Martin Nordio and Cristiano Calcagno and Peter M\"uller and Bertrand Meyer}, title = {Soundness and Completeness of a Program Logic for {E}iffel}, institution = {ETH Zurich}, year = {2009}, number = {617}, urltopdf = {http://se.inf.ethz.ch/people/nordio/papers/NordioCalcagnoMuellerMeyer09.pdf} }