In order to prove software to be correct, predicate calculus with
quantified expressions (for all, exists) is indispensable. The
programming language Modern Eiffel has all possibilities to do
predicate calculus.
The article
http://softwareverificaton.wordpress.com/2012/04/02/83/
describes how reasoning with quantified expressions is done in Modern
Eiffel.