`@NonNull`

.
This is a kind of contract, where the client can use the function
`requires`

and
`ensures`

.✝(There were others,
including `invariant`

,
but I don’t want to get `A`

only when the parameters are positive.
In return, `A`

“promises” that its result
will also be positive.
```
feature { ANY }
f ( a : INTEGER ; b : INTEGER ) : INTEGER
require
a > 0 and then b > 0
do
-- imagine some excellent code here
ensure
Result > 0
end
```

Eiffel has a lot of other nice features, as well, such as provable null safety
(“void safety” in Eiffel terminology).
I’m reasonably sure that Eiffel had this before Rust came along,
but Eiffel doesn’t receive as much attention as Rust.
The checker can prove a program satisfies contracts *at compile-time*,

*or*, if not,

indicate where such a proof falters!

It seems that SPARK does not have a “compiler”
in the traditional sense.
SPARK has a proof checker; you run a separate program on your code
to check that the specified contracts are specified.
When if the proof checker signs off on the code,
you don’t yet have an executable.
To compile SPARK code, one uses the usual Ada compiler.
I ran the examples below using AdaCore’s “GPS”,
an Ada-capable IDE that also works with other languages, such as C++.
It’s relatively to call the proof checker and set its options that way.
It’s also possible to use the command line:
indicate where such a proof falters!

`gnatprove`

will run the proof checker,
and `gnatmake`

will build an executable.
I’ll spare the reader the details of project files,
which lie beyond the scope of this article.
`package`

(in Ada jargon).
It does not implement most features, though; most require a
`package body`

).
However, `Is_Divisible`

is a simple enough function
that we can demonstrate “inline implementation”
of “expression functions”.
(I think I have the Ada jargon correct there.)
```
package Monomials with SPARK_Mode => On is
-- we can turn off SPARK_Mode when needed
type Exponent_Vector is array (Natural range <>) of Natural;
-- this will store exponents
type Monomial (Number_of_Variables: Positive) is record
-- a monomial is little more than an exponent vector,
-- but this can be expanded if need be
Exp: Exponent_Vector(1..Number_of_Variables);
Is_Initialized: Boolean;
end record;
type Term (Number_Of_Variables: Positive) is record
-- a term is the product of a monomial and a coeff
Coeff: Natural;
Mon: Monomial(Number_Of_Variables);
end record;
procedure Init(T: out Monomial; A: in Exponent_Vector) with
Relaxed_Initialization => T,
Pre => (
A'First = 1 and A'First <= A'Last and A'Last = T.Number_of_Variables
),
Post => (
T.Is_Initialized and then T'Initialized and then A = T.Exp
)
;
-- initalizes T's exponents to the values in A
-- notice how the postcondition guarantees initialization!
procedure Set_Exponent(T: in out Monomial; I: in Positive; To: Natural) with
Pre => I <= T.Number_Of_Variables,
Post => T.Exp(I) = To;
-- sets the ith exponent of T to the value of To
function Is_Divisible(First, Second: in Monomial) return Boolean
is ( for all I in Second.Exp'Range => First.Exp(I) >= Second.Exp(I) )
with Pre => (
First.Is_Initialized and then Second.Is_Initialized and then
First.Exp'First = Second.Exp'First and then
First.Exp'Last = Second.Exp'Last
),
Post => (
Is_Divisible'Result =
(
for all I in 1..Second.Number_Of_Variables =>
First.Exp(I) >= Second.Exp(I)
)
);
-- returns True if and only if First is divisible by Second
-- notice how the precondition requires initialization!
function "/" (Num: in Monomial; Den: in Monomial) return Monomial with
Pre => (
Num.Is_Initialized and then Den.Is_Initialized and then
Num.Exp'First = Den.Exp'First and then
Num.Exp'Last = Den.Exp'Last and then
Is_Divisible( Num, Den )
),
Post => (
"/"'Result.Exp'Last = Num.Exp'Last and then
"/"'Result.Number_Of_Variables = Num.Number_Of_Variables and then
( for all I in 1..Den.Number_Of_Variables =>
"/"'Result.Exp(I) = Num.Exp(I) - Den.Exp(I) )
)
;
-- returns the quotient of Monomial and Den
-- notice how the precondition requires divisibility and initialization!
procedure Divide_By(T: in out Monomial; U: in Monomial) with
Pre => (
T.Is_Initialized and then U.Is_Initialized and then
T.Number_Of_Variables = U.Number_Of_Variables and then
T.Exp'First <= T.Exp'Last and then
Is_Divisible(T, U)
),
Post => (
T.Number_Of_Variables = T'Old.Number_Of_Variables and then
( for all I in 1..T.Number_Of_Variables =>
T.Exp(I) = T'Old.Exp(I) - U.Exp(I) )
);
-- divides T by U and stores the result in T
-- notice how the precondition requires divisibility and initialization!
procedure Put(T: in Monomial);
end Monomials;
```

The full package has a lot more, but already you can see
a few interesting points of Ada and SPARK.
- Ada allows the programmer to turn SPARK on and off.
- Ada requires the programmer to be very specific about types:
- it does not usually convert automatically from one type to another,
only from subtypes to supertypes, like
`Natural`

to`Integer`

, and - type compatibility is
*nominal*(by name) rather than*structural*(by the type’s structure).

- it does not usually convert automatically from one type to another,
only from subtypes to supertypes, like
- Arrays don’t have to start at 0.
- Ada allows the programmer to specify the start and end of every array, which is much more convenient than most other languages. It allows indexing to be appropriate for the problem, rather than convenient for the compiler.
- Ada programmers can index array by enumerations as well as integers. I’ve found this to be very useful in many situations, though here it isn’t terribly helpful.

- Preconditions and postconditions can be highly non-trivial,
but can also be expressed rather “naturally”.
Most of the postconditions above contain a
`for all`

expression which verifies everything in the specified range.

`Is_Divisible`

, if I recall correctly.
I think I had originally stated simply that
`First`

’s number of variables had to equal
`Second`

’s number of variables,
but the proof checker would fail.
Let’s look at that function again.
```
function Is_Divisible(First, Second: in Monomial) return Boolean
is ( for all I in Second.Exp'Range => First.Exp(I) >= Second.Exp(I) )
with Pre => (
First.Is_Initialized and then Second.Is_Initialized and then
First.Exp'First = Second.Exp'First and then
First.Exp'Last = Second.Exp'Last
),
Post => (
Is_Divisible'Result =
(
for all I in 1..Second.Number_Of_Variables =>
First.Exp(I) >= Second.Exp(I)
)
);
```

Remember that arrays can start and end anywhere.
The function’s implementation loops
through `Second`

’s exponents,
and checks whether `First`

’s exponent
`Second`

’s.
That `First`

and `Second`

started and ended in different locations,
that loop would have gone outside `First`

’s range.
In short, SPARK saved my bacon here.

Most other languages would not!

Most other languages would not!

```
with Ada.Text_IO; use Ada.Text_IO;
with Ada.Integer_Text_IO; use Ada.Integer_Text_IO;
with Monomials; use Monomials;
procedure Main with SPARK_Mode => On is
O: constant Weight_Vector := Grevlex(5);
T, U: Monomial(5);
V : Monomial := (
Is_Initialized => True,
Number_Of_Variables => 5,
Exp => ( 0, 0, 0, 0, 0 )
);
A: constant Exponent_Vector(1..5) := ( 1, 2, 3, 1, 0);
B: constant Exponent_Vector(1..5) := ( 1 => 1, others => 0 );
begin
-- initialize T and U to the exponents indicated in A and B
Init(T, A);
Init(U, B);
-- let V be the product of T and U
if ( for all I in T.Exp'Range => Natural'Last - U.Exp(I) >= T.Exp(I) ) then
V := T * U;
end if;
Put(V); New_Line;
-- check whether T is divisible by U
if Is_Divisible(T, U) then Put( T / U );
else Put(T); Put(" is not divisible by "); Put(U); New_Line(1);
end if;
New_Line;
-- output a line showing that V is indeed the product of T and U
Put(V); Put(" = "); Put(T); Put(" * "); Put(U); Put("? ");
New_Line;
end Main;
```

Suppose I comment out the first few lines, where I initialize
`T`

and `U`

,
and skip directly to testing if `T`

is divisible by
`U`

.
The proof checker will fail with several errors,
the most interesting for my purposes being the following:
*rr*:*cc* medium: precondition might fail
cannot prove First.Is_Initialized

SPARK detects that the program has failed to satisfy a precondition.
Sloppy initialization has been a frequent source of bugs
in just about any language, at least for me.
`private`

,
and with the requirement of default construction
that most object-oriented languages impose
— as well as many `null`

? could it be dangling?
Is that integer you’re about to divide by zero?)
In many cases, `Gcd`

.
We do not repeat them in the implementation.
```
generic
-- this is a “generic” package specification
-- everything that appears between the keywords “generic”
-- and “package” specifies parameters the client must specify
-- in this case, the client must specify “Ring_Element”,
-- a function to test equality, and a function to computer a remainder
type Ring_Element is private;
-- specifies the type of objects for which we want to compute gcd's;
-- algebraically speaking, this should be a Euclidean Ring.
with function "=" ( Left, Right: Ring_Element ) return Boolean is <>;
-- should returns True iff Left and Right have the same value.
-- the clause “is <>” indicates that the client need not specify “=”
-- if one is commonly available
with function "rem" ( Dividend, Divisor: Ring_Element )
return Ring_Element is <>;
-- returns the remainder of dividing the Dividend by the Divisor;
-- to guarantee termination, the result should be "smaller" than Divisor.
-- how precisely this is accomplished can depend on the ring,
-- and need not be specified.
Zero: Ring_Element;
-- needs to be the ring's additive identity
package Euclidean is
function Gcd(A, B: Ring_Element) return Ring_Element
with
Pre => ( A /= Zero and B /= Zero ),
-- The “Pre”condition indicates that the inputs should be nonzero
Post => ( Gcd'Result /= Zero )
-- The “Post”condition indicates that the result will be nonzero
;
-- returns a greatest common divisor (gcd) of A and B
end Euclidean;
```

```
package body euclidean is
function Gcd(A, B: Ring_Element) return Ring_Element
is
-- initialize local variables
M: Ring_Element := A;
N: Ring_Element := B;
begin
-- loop until the smaller is zero
while N /= Zero loop
declare R: Ring_Element := M rem N;
begin
M := N;
N := R;
end;
end loop;
-- the compiler will give an error if the following statement is missing
return M;
end Gcd;
end euclidean;
```

Here’s an example program that imports our Euclidean package,
(`with`

’s it in
Ada jargon), instantiates a concrete version of the generic,
then uses it to compute the greatest common divisor of two numbers.
```
-- @summary demonstration of SPARK with a generic package
--
-- @author John Perry
--
-- @description
-- Test program for our generic package.
-- packages we need
with Euclidean;
with Ada.Text_IO;
procedure Main
with SPARK_Mode => On
-- setting to On means SPARK will check this procedure when we run GNAT prove
is
package IO is new Ada.Text_IO.Integer_IO ( Num => Integer );
-- instantiating the generic Integer_IO package to make integer output
package Euclidean_ZZ is new Euclidean
(
Ring_Element => Integer,
Zero => 0
);
-- Euclidean_ZZ instantiates our Euclidean package for the integers.
-- The package requires definition of the ring element type
-- and a zero element.
-- It technically requires "=" or "rem" as well, but Ada allows one to define
-- default values for generic parameters, in which case
-- the compiler will substitute those values.
begin
-- print the gcd of -24 and -16, followed by a new line
IO.Put( Euclidean_ZZ.Gcd( -24, -16 ) );
Ada.Text_IO.New_Line;
-- if you uncomment line 46, GNAT prove will report a problem:
--
-- medium: precondition might fail
-- cannot prove B /= 0
--
-- IO.Put( Euclidean_ZZ.Gcd( -24,0 ) );
-- I could avoid fully qualifying the statements above
-- if I resorted to a "use" statement;
-- i.e., "use Euclidean_ZZ" and/or "use Ada.Text_IO.Integer_IO"
-- (the latter defaults to the Integer type).
end Main;
```

If I un-comment the line
`IO.Put( Euclidean_ZZ.Gcd( -24, 0 ) );`

the checker will fail.
From my perspective as a mathematician and programmer who has often struggled
to debug code, `if`

statement.
Technically SPARK `T`

’s and `U`

’s
exponents are known at compile-time.
I get the reason for this