'Ada/SPARK: should I be using GNATprove? Where can I find it?
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?
Solution 1:[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 you hands on SPARK it is to download the GNAT Community Edition from https://www.adacore.com/download which includes GNATprove. The community edition has everything you need to get started wit Ada and SPARK. The main difference of "Pro" is the commercial support.
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|---|
| Solution 1 | Alexander Senier |