Ada: SPARK

GNATprove

Installation

alr install gnatprove

Using GNATprove

gnatprove --solver=z3 -Phello

SPARK-Enabled Packages

package Lib
  with
    SPARK_Mode => On
is

end Lib;

GNU Make Workflow

PROJECT := hello
BUILD   := build
PROVER  := z3

.PHONY: all
all:
     gprbuild -P$(PROJECT)

.PHONY: clean
clean:
     $(RM) -r $(BUILD)
     $(RM) -r lib

.PHONY: prove
prove:
     gnatprove --checks-as-errors=on --prover=$(PROVER) -P$(PROJECT)
     cat $(BUILD)/gnatprove/gnatprove.out