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;

package body Lib
  with
    SPARK_Mode => On
is

...

end Lib;

Example

-- spark_test.ads

package Spark_Test
  with
    SPARK_Mode => On
is

   function Halve
     (X : Integer)
     return Integer
     with
       Global  => null,
       Contract_Cases =>
         (X mod 2  = 0                 => Halve'Result * 2 = X,
          X mod 2 /= 0 and then X >= 0 => Halve'Result * 2 = X - 1,
          X mod 2 /= 0 and then X <  0 => Halve'Result * 2 = X + 1);

   function Square
     (X : Integer)
     return Integer
     with
       Global  => null,
       Pre     => -20000 <= X and then X <= 20000,
       Post    => Square'Result >= 0,
       Contract_Cases =>
         (X  = 0 => Square'Result     = 0,
          X /= 0 => Square'Result / X = X);


   procedure Lemma_Square_Arg_Sign_Irrelevant
     (X : Integer)
     with
       Ghost,
       Global  => null,
       Pre     => -10000 <= X and then X <= 10000;

end Spark_Test;

-- spark_test.adb

package body Spark_Test
  with
    SPARK_Mode => On
is

   function Halve
     (X : Integer)
     return Integer
   is
     (X / 2);

   function Square
     (X : Integer)
     return Integer
   is
     (X * X);

   procedure Lemma_Square_Arg_Sign_Irrelevant
     (X : Integer)
   is
   begin
      pragma Assert (Square (X) = Square (-X));
   end Lemma_Square_Arg_Sign_Irrelevant;

end Spark_Test;

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