Invariante para loop aninhado no programa de multiplicação de matrizes

Estou fazendo uma tese de pós-graduação sobre a comprovação da correção do programa para multiplicar 2 matrizes usando a lógica Hoare. Para fazer isso, preciso gerar o loop invariável para aninhado para este programa:

for i = 1:n
    for j = 1:n
        for k = 1:n
            C(i,j) = A(i,k)*B(k,j) + C(i,j);
        end
    end
end

Tentei encontrar o invariante para o loop interno primeiro, mas não consigo encontrar o verdadeiro até agora. Alguém pode me ajudar a encontrar o invariante para o programa acima?

Você precisa da linha C(i:j) = 0imediatamente antes do loop mais interno; caso contrário, o código está incorreto.

Supondo que a linha esteja no lugar, aqui está a invariante (mais forte possível) imediatamente antes da atribuição no loop mais interno: (Sim, a coisa toda.) O invariante logo após a atribuição tem no lugar de na última soma, mas é idêntico.

$$\begin{align*} C_{IJ} &= \sum_{k=1}^{n} A_{Ik}B_{kJ} & \text{for all $I$ and $J$ such that $1\le I < i$ and $1\le J\le n$} \\ \text{and}~~~ C_{iJ} &= \sum_{k=1}^{n} A_{ik}B_{kJ} & \text{for all $J$ such that $1\le J< j$} \\ \text{and}~~~ C_{ij} &= \sum_{K=1}^{k-1} A_{iK}B_{Kj}. \end{align*}$$ $k$$k-1$

Não existe o "invariável": qualquer loop tem muitos invariantes. Você precisa encontrar um invariante interessante. Como você está tentando provar que o loop calcula uma multiplicação de matrizes, seu invariante deve implicar que quando , os coeficientes de são os do produto da matriz , ou seja, É bastante natural para especializar esta propriedade de e de conjecturar uma invariante para as espiras externas e meio:$i=j=k=n$$C$$A \times B$

$$\forall i \in [1,n], \forall j \in [1,n], C(i,j) = \sum_{k=1}^n A(i,k) \cdot B(k,j)$$ $i$$j$

• $\forall j \in [1,n], C(i,j) = \sum_{k=1}^n A(i,k) \cdot B(k,j)$ no loop externo
• $C(i,j) = \sum_{k=1}^n A(i,k) \cdot B(k,j)$ no loop do meio

Cada execução do loop interno adiciona o ésimo termo à soma, o que leva ao invariante proposto: É fácil ver que, se essa invariante é mantida, a invariante proposta para o loop intermediário é mantida e, a partir disso, a invariante proposta para o loop externo é mantida e o programa faz o que é esperado.$k$

$$C(i,j) = \sum_{l=1}^k A(i,l) \cdot B(l,j)$$

O que falta provar é a condição inicial. Você precisa provar que , ou seja, na entrada do programa. É melhor inicializar para que seja assim. Como alternativa, você pode obter essa propriedade fazendo a inicialização dentro do loop intermediário, imediatamente antes de entrar no loop interno.$\forall i, \forall j, C(i,j) = \sum_{l=1}^0 A(i,l) \cdot B(l,j)$$\forall i, \forall j, C(i,j) = 0$$C$