## Euler Project problem 11, SPARK/Ada version

Find in a matrix the four numbers, adjacent in the same direction, that maximize their product.

The ZIP file below contains all the necessary source file to compile the code using GNAT and redo the proofs using SPARK.

Authors: Sylvain Dailler

Topics: Matrices

Tools: SPARK 2014

References: Project Euler / ProofInUse joint laboratory

see also the index (by topic, by tool, by reference, by year)

This is first the Ada interface, with the protoype of the main procedure 'Max_Product_4', but also the pre- and post-condition, using the regular Ada 2012 syntax. pe11_max4.ads

```package PE11_Max4
with SPARK_Mode
is

-- The objective of this project is to find the maximum product of four
-- consecutive elements of a matrix in any directions (lines, columns and
-- diagonals). The direction for each product is decided by the
-- 2 first elements.
-- We solve it by exploring each directions of 4 elements for every
-- element of the matrix

--  Could use big_int and go beyond 10000 I guess
--  or trust the ada/spark compiler flag dedicated to this
subtype Small_Integer is Long_Integer range -10_000 .. 10_000;

subtype Range_Integer is Integer range 1 .. Integer'Last - 3;

type Direction is (RD, LD, RIGHT, DOWN);

-- Definition of the matrix with suitable range to take care of
-- possible overflow of possible addition of indices
type Matrix is array (Range_Integer range <>, Range_Integer range <>)
of Small_Integer;

-- A product in a direction D beginning at (I, J) is valid iff
-- each element of the product actually is in the matrix.
function Is_Valid (M : Matrix; I, J : Range_Integer; D : Direction)
return Boolean is
(I in M'Range(1) and J in M'Range(2) and
(case D is
when RD    => I + 3 in M'Range(1) and J + 3 in M'Range(2),
when LD    => I + 3 in M'Range(1) and J - 3 in M'Range(2),
when RIGHT => J + 3 in M'Range(2),
when DOWN  => I + 3 in M'Range(1)));

-- Product in the four given directions

function Right_Diag (M : Matrix; I, J : Range_Integer) return Long_Integer is
(M (I, J) * M (I + 1, J + 1) * M (I + 2, J + 2) * M (I + 3, J + 3)) with
Pre => Is_Valid (M, I, J, RD);

function Left_Diag (M: Matrix; I, J: Range_Integer) return Long_Integer is
(M (I, J) * M (I + 1, J - 1) * M (I + 2, J - 2) * M (I + 3, J - 3)) with
Pre => Is_Valid (M, I, J, LD);

function Column (M: Matrix; I, J: Range_Integer) return Long_Integer is
(M (I, J) * M (I + 1, J) * M (I + 2, J) * M (I + 3, J)) with
Pre => Is_Valid (M, I, J, DOWN);

function Line (M: Matrix; I, J: Range_Integer) return Long_Integer is
(M (I, J) * M (I, J + 1) * M (I, J + 2) * M (I, J + 3)) with
Pre => Is_Valid (M, I, J, RIGHT);

function Mult_Value (M : Matrix; I, J : Range_Integer; D : Direction)
return Long_Integer is
(case D is
when RD => Right_Diag (M, I, J),
when LD => Left_Diag (M, I, J),
when RIGHT => Line (M, I, J),
when DOWN => Column (M, I, J))
with Pre => Is_Valid (M, I, J, D);

-- Function returning the maximum product.
-- Matrix must be a reasonible matrix
-- Max definition is:
-- - the result must be greater than any valid product of 4 elements
-- - the result should be attained by a given product
function Max_Product_4 (M: Matrix) return Long_Integer with
Pre => M'Length(1) >= 4 and M'Length(2) >= 4,
Post =>
(for all I in M'Range (1) =>
(for all J in M'Range (2) =>
(for all D in Direction =>
(if Is_Valid (M, I, J, D) then Mult_Value (M, I, J, D) <= Max_Product_4'Result))))
and
(for some I in M'Range (1) =>
(for some J in M'Range (2) =>
(for some D in Direction =>
(Is_Valid (M, I, J, D) and then Mult_Value (M, I, J, D) = Max_Product_4'Result))));

end PE11_Max4;
```

This is then the body, with the code of the main procedure 'Max_Product_4'. pe11_max4.adb

```
package Body Pe11_Max4 is

function Max_Product_4 (M: Matrix) return Long_Integer is
Cur_Max : Long_Integer := Right_Diag (M, M'First (1), M'First (2));
-- Current position (Cur_I, Cur_J) and direction D always resulting
-- in a product equal to Cur_max
Cur_I : Integer range M'Range(1) := M'First (1) with Ghost;
Cur_J : Integer range M'Range(2) := M'First(2) with Ghost;
D: Direction := RD with Ghost;
begin
for I in M'Range (1) loop
-- Loop_invariant: Current max should be accessible by an already
-- attained (Cur_I, Cur_J, D)
pragma Loop_Invariant (Is_Valid (M, Cur_I, Cur_J, D));
pragma Loop_Invariant (Mult_Value (M, Cur_I, Cur_J, D) = Cur_Max);

-- Loop_invariant: Current max should be greater than each already
-- accessed product ie all (I', J, D) with I' < I, and for all J and D
pragma Loop_Invariant
(for all K in M'First (1) .. (I - 1) =>
(for all L in M'Range (2) =>
(for all D1 in Direction =>
(if Is_Valid (M, K, L, D1) then Cur_Max >= Mult_Value (M, K, L, D1)))));

for J in M'Range (2) loop
-- Loop_invariant: Current max should be accessible by an already
-- attained (Cur_I, Cur_J, D)
pragma Loop_Invariant (Is_Valid (M, Cur_I, Cur_J, D));
pragma Loop_Invariant (Mult_Value (M, Cur_I, Cur_J, D) = Cur_Max);

-- Loop_invariant: Current max should be greater than each already
-- accessed product:  all (I', J', D) with I' < I for all J' and D
-- or I' = I and J' < J for all D
pragma Loop_Invariant
(for all K in M'First (1) .. I =>
(for all L in M'Range (2) =>
(for all D1 in Direction =>
(if K < I or L < J then
(if Is_Valid (M, K, L, D1) then Cur_Max >= Mult_Value (M, K, L, D1))))));
-- Checking of the 4 directions
-- Right_diag
if (I + 3 <= M'Last (1) and J + 3 <= M'Last (2)) then
if (Right_Diag(M, I, J) > Cur_Max) then
Cur_I := I;
Cur_J := J;
D := RD;
Cur_Max := Right_Diag (M, I, J);
end if;
end if;
-- Left_diag
if (I + 3 <= M'Last(1) and J - 3 >= M'First(2)) then
if (Left_Diag(M, I, J) > Cur_Max) then
Cur_I := I;
Cur_J := J;
D := LD;
Cur_Max := Left_diag (M, I, J);
end if;
end if;
-- Column
if (I + 3 <= M'Last(1)) then
if (Column(M, I, J) > Cur_Max) then
Cur_I := I;
Cur_J := J;
D := DOWN;
Cur_Max := Column (M, I, J);
end if;
end if;
-- Line
if (J + 3 <= M'Last (2)) then
if (Line(M, I, J) > Cur_Max) then
Cur_I := I;
Cur_J := J;
D := RIGHT;
Cur_Max := Line (M, I, J);
end if;
end if;
end loop;
end loop;
return Cur_Max;
end;

end PE11_Max4;
```

Finally, here is a simple test. This part produces output, outside the SPARK fragment, so not analyzed by the proof tools. main.adb

```--  with Pe11; use Pe11;
with Pe11_Max4; use PE11_Max4;

procedure Main is
M: Matrix :=
((08, 02, 22, 97, 38, 15, 00, 40, 00, 75, 04, 05, 07, 78, 52, 12, 50, 77, 91, 08),
(49, 49, 99, 40, 17, 81, 18, 57, 60, 87, 17, 40, 98, 43, 69, 48, 04, 56, 62, 00),
(81, 49, 31, 73, 55, 79, 14, 29, 93, 71, 40, 67, 53, 88, 30, 03, 49, 13, 36, 65),
(52, 70, 95, 23, 04, 60, 11, 42, 69, 24, 68, 56, 01, 32, 56, 71, 37, 02, 36, 91),
(22, 31, 16, 71, 51, 67, 63, 89, 41, 92, 36, 54, 22, 40, 40, 28, 66, 33, 13, 80),
(24, 47, 32, 60, 99, 03, 45, 02, 44, 75, 33, 53, 78, 36, 84, 20, 35, 17, 12, 50),
(32, 98, 81, 28, 64, 23, 67, 10, 26, 38, 40, 67, 59, 54, 70, 66, 18, 38, 64, 70),
(67, 26, 20, 68, 02, 62, 12, 20, 95, 63, 94, 39, 63, 08, 40, 91, 66, 49, 94, 21),
(24, 55, 58, 05, 66, 73, 99, 26, 97, 17, 78, 78, 96, 83, 14, 88, 34, 89, 63, 72),
(21, 36, 23, 09, 75, 00, 76, 44, 20, 45, 35, 14, 00, 61, 33, 97, 34, 31, 33, 95),
(78, 17, 53, 28, 22, 75, 31, 67, 15, 94, 03, 80, 04, 62, 16, 14, 09, 53, 56, 92),
(16, 39, 05, 42, 96, 35, 31, 47, 55, 58, 88, 24, 00, 17, 54, 24, 36, 29, 85, 57),
(86, 56, 00, 48, 35, 71, 89, 07, 05, 44, 44, 37, 44, 60, 21, 58, 51, 54, 17, 58),
(19, 80, 81, 68, 05, 94, 47, 69, 28, 73, 92, 13, 86, 52, 17, 77, 04, 89, 55, 40),
(04, 52, 08, 83, 97, 35, 99, 16, 07, 97, 57, 32, 16, 26, 26, 79, 33, 27, 98, 66),
(88, 36, 68, 87, 57, 62, 20, 72, 03, 46, 33, 67, 46, 55, 12, 32, 63, 93, 53, 69),
(04, 42, 16, 73, 38, 25, 39, 11, 24, 94, 72, 18, 08, 46, 29, 32, 40, 62, 76, 36),
(20, 69, 36, 41, 72, 30, 23, 88, 34, 62, 99, 69, 82, 67, 59, 85, 74, 04, 36, 16),
(20, 73, 35, 29, 78, 31, 90, 01, 74, 31, 49, 71, 48, 86, 81, 16, 23, 57, 05, 54),
(01, 70, 54, 71, 83, 51, 54, 69, 16, 92, 33, 48, 61, 43, 52, 01, 89, 19, 67, 48));

begin
Put_Line(Long_Integer'Image (Max_Product_4(M)));
end;

```

# Why3 Proof Results for Project "pe11_max4"

## Theory "pe11_max4.Pe11_max4__package_def": fully verified in 0.00 s

 Obligations VC for def split_goal_wp

## Theory "pe11_max4.Pe11_max4__is_valid__subprogram_def": fully verified in 0.11 s

 Obligations Z3 (4.4.1) VC for def --- split_goal_wp 1. precondition 0.01 2. precondition 0.01 3. precondition 0.01 4. precondition 0.02 5. precondition 0.01 6. precondition 0.01 7. precondition 0.01 8. precondition 0.01 9. precondition 0.01 10. precondition 0.01

## Theory "pe11_max4.Pe11_max4__right_diag__subprogram_def": fully verified in 0.17 s

 Obligations Z3 (4.4.1) VC for def --- split_goal_wp 1. precondition 0.01 2. assertion 0.01 3. precondition 0.01 4. assertion 0.02 5. assertion 0.01 6. assertion 0.02 7. assertion 0.01 8. assertion 0.01 9. assertion 0.01 10. assertion 0.02 11. precondition 0.01 12. precondition 0.01 13. precondition 0.02

## Theory "pe11_max4.Pe11_max4__left_diag__subprogram_def": fully verified in 0.18 s

 Obligations Z3 (4.4.1) VC for def --- split_goal_wp 1. assertion 0.02 2. precondition 0.01 3. assertion 0.01 4. assertion 0.01 5. assertion 0.01 6. assertion 0.01 7. assertion 0.02 8. assertion 0.02 9. assertion 0.02 10. precondition 0.02 11. precondition 0.01 12. precondition 0.02

## Theory "pe11_max4.Pe11_max4__column__subprogram_def": fully verified in 0.15 s

 Obligations Z3 (4.4.1) VC for def --- split_goal_wp 1. assertion 0.01 2. precondition 0.01 3. assertion 0.01 4. assertion 0.01 5. assertion 0.01 6. assertion 0.01 7. assertion 0.02 8. assertion 0.01 9. assertion 0.01 10. precondition 0.02 11. precondition 0.01 12. precondition 0.02

## Theory "pe11_max4.Pe11_max4__line__subprogram_def": fully verified in 0.17 s

 Obligations Z3 (4.4.1) VC for def --- split_goal_wp 1. precondition 0.01 2. assertion 0.01 3. assertion 0.02 4. assertion 0.01 5. assertion 0.01 6. assertion 0.02 7. assertion 0.01 8. assertion 0.02 9. assertion 0.01 10. precondition 0.02 11. precondition 0.01 12. precondition 0.02

## Theory "pe11_max4.Pe11_max4__mult_value__subprogram_def": fully verified in 0.06 s

 Obligations Z3 (4.4.1) VC for def --- split_goal_wp 1. precondition 0.01 2. precondition 0.01 3. precondition 0.02 4. precondition 0.02

## Theory "pe11_max4.Pe11_max4__max_product_4__subprogram_def": fully verified in 0.00 s

 Obligations VC for def split_goal_wp