Wiki Agenda Contact English version

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. pe11_max4.ads

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;

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

File : 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

File : main.adb


--  with Pe11; use Pe11;
with Pe11_Max4; use PE11_Max4;
with Ada.Text_IO; use Ada.Text_IO;

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

ObligationsZ3 (4.4.1)
VC for def---
split_goal_wp
  1. precondition0.01
2. precondition0.01
3. precondition0.01
4. precondition0.02
5. precondition0.01
6. precondition0.01
7. precondition0.01
8. precondition0.01
9. precondition0.01
10. precondition0.01

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

ObligationsZ3 (4.4.1)
VC for def---
split_goal_wp
  1. precondition0.01
2. assertion0.01
3. precondition0.01
4. assertion0.02
5. assertion0.01
6. assertion0.02
7. assertion0.01
8. assertion0.01
9. assertion0.01
10. assertion0.02
11. precondition0.01
12. precondition0.01
13. precondition0.02

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

ObligationsZ3 (4.4.1)
VC for def---
split_goal_wp
  1. assertion0.02
2. precondition0.01
3. assertion0.01
4. assertion0.01
5. assertion0.01
6. assertion0.01
7. assertion0.02
8. assertion0.02
9. assertion0.02
10. precondition0.02
11. precondition0.01
12. precondition0.02

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

ObligationsZ3 (4.4.1)
VC for def---
split_goal_wp
  1. assertion0.01
2. precondition0.01
3. assertion0.01
4. assertion0.01
5. assertion0.01
6. assertion0.01
7. assertion0.02
8. assertion0.01
9. assertion0.01
10. precondition0.02
11. precondition0.01
12. precondition0.02

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

ObligationsZ3 (4.4.1)
VC for def---
split_goal_wp
  1. precondition0.01
2. assertion0.01
3. assertion0.02
4. assertion0.01
5. assertion0.01
6. assertion0.02
7. assertion0.01
8. assertion0.02
9. assertion0.01
10. precondition0.02
11. precondition0.01
12. precondition0.02

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

ObligationsZ3 (4.4.1)
VC for def---
split_goal_wp
  1. precondition0.01
2. precondition0.01
3. precondition0.02
4. precondition0.02

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

Obligations
VC for def
split_goal_wp