@Techreport{NordioCalcagnoMuellerMeyer09, author = {M. Nordio and C. Calcagno and P. M\"uller and B. Meyer}, title = {Soundness and Completeness of a Program Logic for {E}iffel}, institution = {ETH Zurich}, year = {2009}, number = {617} }