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.
Auteurs: Sylvain Dailler
Catégories: Matrices
Outils: SPARK 2014
Références: Project Euler / ProofInUse joint laboratory
Voir aussi: 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
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;