## 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:** Maximal sum in a matrix / Maximize product of adjacent numbers in a matrix

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

download ZIP archive

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.

# File : pe11_max4.ads

packagePE11_Max4withSPARK_Modeis-- 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 thissubtypeSmall_IntegerisLong_Integerrange-10_000 .. 10_000;subtypeRange_IntegerisIntegerrange1 .. Integer'Last - 3;typeDirectionis(RD, LD, RIGHT, DOWN);-- Definition of the matrix with suitable range to take care of-- possible overflow of possible addition of indicestypeMatrixisarray(Range_Integerrange<>, Range_Integerrange<>)ofSmall_Integer;-- A product in a direction D beginning at (I, J) is valid iff-- each element of the product actually is in the matrix.functionIs_Valid (M : Matrix; I, J : Range_Integer; D : Direction)returnBooleanis(IinM'Range(1)andJinM'Range(2)and(caseDiswhenRD => I + 3inM'Range(1)andJ + 3inM'Range(2),whenLD => I + 3inM'Range(1)andJ - 3inM'Range(2),whenRIGHT => J + 3inM'Range(2),whenDOWN => I + 3inM'Range(1)));-- Product in the four given directionsfunctionRight_Diag (M : Matrix; I, J : Range_Integer)returnLong_Integeris(M (I, J) * M (I + 1, J + 1) * M (I + 2, J + 2) * M (I + 3, J + 3))withPre => Is_Valid (M, I, J, RD);functionLeft_Diag (M: Matrix; I, J: Range_Integer)returnLong_Integeris(M (I, J) * M (I + 1, J - 1) * M (I + 2, J - 2) * M (I + 3, J - 3))withPre => Is_Valid (M, I, J, LD);functionColumn (M: Matrix; I, J: Range_Integer)returnLong_Integeris(M (I, J) * M (I + 1, J) * M (I + 2, J) * M (I + 3, J))withPre => Is_Valid (M, I, J, DOWN);functionLine (M: Matrix; I, J: Range_Integer)returnLong_Integeris(M (I, J) * M (I, J + 1) * M (I, J + 2) * M (I, J + 3))withPre => Is_Valid (M, I, J, RIGHT);functionMult_Value (M : Matrix; I, J : Range_Integer; D : Direction)returnLong_Integeris(caseDiswhenRD => Right_Diag (M, I, J),whenLD => Left_Diag (M, I, J),whenRIGHT => Line (M, I, J),whenDOWN => Column (M, I, J))withPre => 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 productfunctionMax_Product_4 (M: Matrix)returnLong_IntegerwithPre => M'Length(1) >= 4andM'Length(2) >= 4, Post => (forallIinM'Range(1) => (forallJinM'Range(2) => (forallDinDirection => (ifIs_Valid (M, I, J, D)thenMult_Value (M, I, J, D) <= Max_Product_4'Result))))and(forsome IinM'Range(1) => (forsome JinM'Range(2) => (forsome DinDirection => (Is_Valid (M, I, J, D)andthenMult_Value (M, I, J, D) = Max_Product_4'Result))));endPE11_Max4;

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

# File : pe11_max4.adb

packageBodyPe11_Max4isfunctionMax_Product_4 (M: Matrix)returnLong_IntegerisCur_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_maxCur_I : IntegerrangeM'Range(1) := M'First (1)withGhost; Cur_J : IntegerrangeM'Range(2) := M'First(2)withGhost; D: Direction := RDwithGhost;beginforIinM'Range(1)loop-- Loop_invariant: Current max should be accessible by an already-- attained (Cur_I, Cur_J, D)pragmaLoop_Invariant (Is_Valid (M, Cur_I, Cur_J, D));pragmaLoop_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 DpragmaLoop_Invariant (forallKinM'First (1) .. (I - 1) => (forallLinM'Range(2) => (forallD1inDirection => (ifIs_Valid (M, K, L, D1)thenCur_Max >= Mult_Value (M, K, L, D1)))));forJinM'Range(2)loop-- Loop_invariant: Current max should be accessible by an already-- attained (Cur_I, Cur_J, D)pragmaLoop_Invariant (Is_Valid (M, Cur_I, Cur_J, D));pragmaLoop_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 DpragmaLoop_Invariant (forallKinM'First (1) .. I => (forallLinM'Range(2) => (forallD1inDirection => (ifK < IorL < Jthen(ifIs_Valid (M, K, L, D1)thenCur_Max >= Mult_Value (M, K, L, D1))))));-- Checking of the 4 directions-- Right_diagif(I + 3 <= M'Last (1)andJ + 3 <= M'Last (2))thenif(Right_Diag(M, I, J) > Cur_Max)thenCur_I := I; Cur_J := J; D := RD; Cur_Max := Right_Diag (M, I, J);endif;endif;-- Left_diagif(I + 3 <= M'Last(1)andJ - 3 >= M'First(2))thenif(Left_Diag(M, I, J) > Cur_Max)thenCur_I := I; Cur_J := J; D := LD; Cur_Max := Left_diag (M, I, J);endif;endif;-- Columnif(I + 3 <= M'Last(1))thenif(Column(M, I, J) > Cur_Max)thenCur_I := I; Cur_J := J; D := DOWN; Cur_Max := Column (M, I, J);endif;endif;-- Lineif(J + 3 <= M'Last (2))thenif(Line(M, I, J) > Cur_Max)thenCur_I := I; Cur_J := J; D := RIGHT; Cur_Max := Line (M, I, J);endif;endif;endloop;endloop;returnCur_Max;end;endPE11_Max4;

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

# File : main.adb

-- with Pe11; use Pe11;withPe11_Max4;usePE11_Max4;withAda.Text_IO;useAda.Text_IO;procedureMainisM: 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));beginPut_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 |