SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Proving Loops Without Loop Invariants

by Yannick Moy in Formal Verification – July 20, 2017

For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to facilitate writing loop invariants by improving the documentation and the technology in different ways, but writing loops invariants remains difficult sometimes, in particular for beginners. To completely remove the need for loop invariants in simple cases, we have implemented loop unrolling in GNATprove. It turns out it is quite powerful when applicable.