[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification VerifyThis3-sequential
specification
   

   

   

   using matrixops, 
         sparsearray

   

   

   

   

   
   
   functions  . .toMatrix ( . ) : sparsearray × nat × nat → matrix;
   predicates  okspmx : sparsearray × nat × nat;
   procedures MULT# sparsearray × nat × vector :  : vector  nondeterministic;
   variables  r : nat;
              c : nat;
              spmx : sparsearray;
              x : vector;
              y : vector;
              m : nat;
              n : nat;
              a : elem;
              np : natpair;
   
   

   

   axioms okspmx-def :  ⊦ okspmx(spmx, r, c) ↔ (∀ np. np ∈ spmx → np.r < r ∧ np.c < c);
          toMatrix-rowno :  ⊦ #r spmx.toMatrix(r, c) = r;
          used for: s, ls;
          toMatrix-colno :  ⊦ #c spmx.toMatrix(r, c) = c;
          used for: s, ls;
          toMatrix-get :  ⊦ m < r ∧ n < c → spmx.toMatrix(r, c)[m, n] = (m × n ∈ spmx ⊃ spmx[m × n];O);
          used for: s, ls;
          init :  ⊦ m < n → mkvector(n)[m] = O;
          used for: s, ls;
          comment: fixes the initial content of mkarray (usually unspecified);

   theorems correct : okspmx(spmx, r, # x) ⊦ ⟪MULT#(spmx, r, x; ; y)⟫ (y = spmx.toMatrix(r, # x) * x);

   declarations MULT
                : MULT#(spmx, r, x; ; y)
                  {y := mkvector(r); 
                   while spmx ≠ ∅
                   do {/* _:
                          invariant y + spmx.toMatrix(r, # x) * x = (spmx`).toMatrix(r, # x) * x ∧ spmx ⊆ spmx` ∧ # y = r
                          wfbound # spmx; 
                       */; 
                       choose np with np ∈ spmx in {y[np.r] := y[np.r] + spmx[np] * x[np.c]; spmx := spmx -- np}}
                  }
                ;
end specification