Re: matrix manipulation

[Simon Wright <simon@pushface.org>]

hnptz@yahoo.de writes:

> Hi,
>
> I would like to solve the following Ada-Programming demand:
>
> bk :=3; Dv := 4;
>
> H : Real_Matrix(1..bk*Dv,1..bk*Dv);
>
> type Block_Matrix
>    is array (Positive range <>, Positive range <>) of Real_Matrix(1..Dv,1..Dv);
>
> HB : Block_Matrix(1..bk,1..bk);
>
> Now, there are 12 Block_Matrices which make up H. After calculation of
> all HB's I want to place them into H and ended up in coding of 8
> different for loops. Is there a more elegant solution? I noticed that
> slicing would only work with a definition of linear arrays of a linear
> array, which does not fit for the rest of my program.

You might find this package helpful. I haven't been able to prove the
postconditions, due to lack of SPARK smarts, but see the demo.

--

package Block_Matrices
  with SPARK_Mode
is

   pragma Assertion_Policy (Check);

   type Matrix is array (Positive range <>, Positive range <>) of Integer;

   function Submatrix (Of_Matrix : Matrix;
                       At_Row    : Positive;
                       At_Column : Positive;
                       Rows      : Natural;
                       Columns   : Natural) return Matrix
   with
     Pre => At_Row in Of_Matrix'Range (1)
            and At_Column in Of_Matrix'Range (2)
            and At_Row + (Rows - 1) in Of_Matrix'Range (1)
            and At_Column + (Columns - 1) in Of_Matrix'Range (2),
     Post => Submatrix'Result'First (1) = At_Row
             and Submatrix'Result'Length (1) = Rows
             and Submatrix'Result'First (2) = At_Column
             and Submatrix'Result'Length (2) = Columns
             and (for all J in Submatrix'Result'Range (1) =>
                    (for all K in Submatrix'Result'Range (2) =>
                       Submatrix'Result (J, K) = Of_Matrix (J, K)));

   procedure Assign (Submatrix : Matrix; To : in out Matrix)
   with
     Pre => Submatrix'First (1) in To'Range (1)
            and Submatrix'Last (1) in To'Range (1)
            and Submatrix'First (2) in To'Range (2)
            and Submatrix'Last (2) in To'Range (2),
     Post => (for all J in Submatrix'Range (1) =>
                (for all K in Submatrix'Range (2) =>
                   To (J, K) = Submatrix (J, K)));

end Block_Matrices;

package body Block_Matrices
with SPARK_Mode
is

   function Submatrix (Of_Matrix : Matrix;
                       At_Row    : Positive;
                       At_Column : Positive;
                       Rows      : Natural;
                       Columns   : Natural) return Matrix
   is
   begin
      return Result : Matrix
        (At_Row .. At_Row - 1 + Rows, At_Column .. At_Column - 1 + Columns) do
         for J in Result'Range (1) loop
            for K in Result'Range (2) loop
               Result (J, K) := Of_Matrix (J, K);
            end loop;
         end loop;
      end return;
   end Submatrix;

   procedure Assign (Submatrix : Matrix; To : in out Matrix)
   is
   begin
      for J in Submatrix'Range (1) loop
         for K in Submatrix'Range (2) loop
            To (J, K) := Submatrix (J, K);
         end loop;
      end loop;
   end Assign;

end Block_Matrices;

with Ada.Text_IO; use Ada.Text_IO;
procedure Block_Matrices.Test
is

   procedure Print (M : Matrix) is
   begin
      for R in M'Range (1) loop
         for C in M'Range (2) loop
            Put (" " & M (R, C)'Image);
         end loop;
         New_Line;
      end loop;
   end Print;

   M : Matrix (1 .. 8, 1 .. 8);

begin

   for J in M'Range (1) loop
      for K in M'Range (2) loop
         M (J, K) := J * K;
      end loop;
   end loop;

   declare
      S : Matrix := Submatrix (M, 3, 5, 2, 3);
   begin
      Print (S);
      New_Line;
      for El of S loop
         El := - El;
      end loop;
      Assign (S, M);
      Print (M);
   end;

end Block_Matrices.Test;