alt : http://old-courses.cn.ntua.gr/file.php/61/ch7hoare_h.pdf