Ada/SPARK: should I be using GNATprove? Where can I find it?

Question

On chapter 22.1 of this Learning Ada, trying to build the examples.

It expects GNATprove to be installed. I am using Ubuntu 18.04 LTS, and I don't see any package that provides it. When I tried to find the main repo, all I found was something at Open Do, and when I click the download button, it appears to be a broken link. Google has little to offer about GNATprove, which is a bit worrying.

I'm new to Ada so I don't really know what I should be using, so if GNATprove is not the right thing, then let me know. I'm also generally expecting a free software toolchain -- is that a reasonable expectation or should I expect to need the "pro" version to see what Ada/SPARK are all about?

Answer 1

GNATprove is the tool used for the formal verification of SPARK, i.e. the provable subset of Ada. If you want to build reliable software and be sure that it does the right thing, it's certainly worth looking at SPARK!

The easiest way to get your hands on SPARK is to install the Community Edition using Alire. Alternatively, you can download and install GNATprove manually from GitHub. More details can be found in the SPARK project on GitHub. The community edition has everything you need to get started wit Ada and SPARK. The main difference of "Pro" is the commercial support.