Specification multiply

[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,
enrich
   matrix-dot
with
   

   
   
   
   
   procedures multiply matrix × matrix : matrix  ;
   
   
   

   

   

   

   declarations multiply
                : multiply(A, B; C)
                  {C := A.rows × B.cols; 
                   let m = 0
                   in while m < C.rows
                      do {/* (correctness
                              invariant:   m ≤ C.rows ∧ C.rows = A.rows ∧ C.cols = B.cols
                                         ∧ (∀ m0, n0. 
                                                m0 < C.rows ∧ n0 < C.cols
                                              → C[m0, n0] = (C`)[m0, n0] + (m0 < m ∧ n0 < C.cols ⊃ Σ(B.rows, λ k. A[m0, k] * B[k, n0]);0))
                              wfbound: C.rows - m)
                          */; 
                          let k = 0
                          in while k < B.rows
                             do {/* (correctness
                                     invariant:   k ≤ B.rows ∧ C.rows = A.rows ∧ C.cols = B.cols
                                                ∧ (∀ m0, n0. 
                                                       m0 < C.rows ∧ n0 < C.cols
                                                     → C[m0, n0] = (C`)[m0, n0] + (m0 = m ∧ n0 < C.cols ⊃ Σ(k, λ k. A[m0, k] * B[k, n0]);0))
                                     wfbound: B.rows - k)
                                 */; 
                                 let n = 0
                                 in while n < C.cols
                                    do {/* (correctness
                                            invariant:   n ≤ C.cols ∧ C.rows = A.rows ∧ C.cols = B.cols
                                                       ∧ (∀ m0, n0. 
                                                              m0 < C.rows ∧ n0 < C.cols
                                                            → C[m0, n0] = (C`)[m0, n0] + (m0 = m ∧ n0 < n ⊃ A[m0, k] * B[k, n0];0))
                                            wfbound: C.cols - n)
                                        */; 
                                        C[m, n] := C[m, n] + A[m, k] * B[k, n]; n := n + 1}; 
                                 k := k + 1}; 
                          m := m + 1}
                  }
                ;
end enrich