Wagner, Silke Programming Logics, MPI for Informatics, Max Planck Society;
Wagner, S.(2004). Summaries for while programs with recursion (MPI-I-2004-2-007). Saarbrücken: Max-Planck-Institut für Informatik.