SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

GNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)

by Yannick Moy in Formal Verification – April 6, 2017

Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first algorithms that humans devised. So it's quite appealing to try to prove it with an automatic proving toolset like SPARK. It turns out that proving it automatically is not so easy, just like understanding why it works is not so easy. In this post, I am using ghost code to prove correct implementations of the GCD, starting from a naive linear search algorithm and ending with Euclid's algorithm.