Eiffel has loop invariants, for example see: http://se.ethz.ch/~meyer/publications/methodology/invariants.pdf http://se.ethz.ch/~meyer/publications/methodology

Eiffel has loop invariants, for example see: http://se.ethz.ch/~meyer/publications/methodology/invariants.pdf http://se.ethz.ch/~meyer/publications/methodology/invariants... Also see Meyer's Design By Contract book, which you should read even if you will never use Eiffel - it's a gem.