Invariante für verschachtelte Schleife im Matrix-Multiplikationsprogramm

Ich mache eine Abschlussarbeit über den Nachweis der Richtigkeit des Programms zum Multiplizieren von 2 Matrizen mit Hoare-Logik. Dazu muss ich die Invariante für die verschachtelte Schleife für dieses Programm generieren:

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

Ich habe zuerst versucht, die Invariante für die innere Schleife zu finden, aber ich kann die wahre bis jetzt nicht finden. Kann mir jemand helfen, die Invariante für das obige Programm zu finden?

Sie benötigen die Linie C(i:j) = 0kurz vor der innersten Schleife. Andernfalls ist der Code falsch.

Unter der Annahme, dass diese Linie vorhanden ist, ist hier die (stärkste mögliche) Invariante unmittelbar vor der Zuweisung in der innersten Schleife: (Ja, das Ganze.) Die Invariante unmittelbar nach der Zuweisung hat anstelle von in der letzten Summe, ist aber ansonsten identisch.

$$\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$

Es gibt keine "die" Invariante: Jede Schleife hat viele Invarianten. Sie müssen eine interessante Invariante finden. Da Sie versuchen zu beweisen, dass die Schleife eine Matrixmultiplikation berechnet, muss Ihre Invariante implizieren, dass wenn , die Koeffizienten von diejenigen des Matrixprodukts , dh Es ist eher Natürlich, um diese Eigenschaft von und zu spezialisieren und eine Invariante für die äußere und mittlere Schleife zu vermuten:$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)$ auf der äußeren Schleife
• $C(i,j) = \sum_{k=1}^n A(i,k) \cdot B(k,j)$ in der mittleren Schleife

Jeder Lauf der inneren Schleife addiert den ten Term zur Summe, was zur vorgeschlagenen Invariante führt: Es ist leicht zu erkennen, dass, wenn diese Invariante gilt, die vorgeschlagene Invariante für die mittlere Schleife gilt und daraus die vorgeschlagene Invariante für die äußere Schleife gilt und das Programm das tut, was erwartet wird.$k$

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

Was noch bewiesen werden muss, ist der Ausgangszustand. Sie müssen beweisen, dass , dh beim Eintritt in das Programm. Sie sollten besser initialisieren, damit dies so ist. Alternativ können Sie diese Eigenschaft erreichen, indem Sie die Initialisierung innerhalb der mittleren Schleife unmittelbar vor dem Eintritt in die innere Schleife durchführen.$\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$