Seite 1 von 1

Theorietestat 4: Korrektheitsbeweis SumMatrix

Verfasst: 27. Jun 2017 21:11
von Cem
Hi,

im o.g. Beispiel wird bei der Betrachtung der äußeren Schleife in der Spezifikation ein Output erwähnt, die Summe der Matrixelemente. Ich denke aber eher dass die innere Schleife diesen Output liefert, was dann sowas wie das "Ergebnis aus der Blackbox" wäre. Liege ich da falsch?

Re: Theorietestat 4: Korrektheitsbeweis SumMatrix

Verfasst: 27. Jun 2017 21:46
von invariant
Hallo,

die innere Schleife liefert in diesem Sinn keinen Output - daher ist der "Output" für diese in den Nachbedingungen verarbeitet.
Mit dem Beweis der äußeren Schleife wird hier auch der ganze Algorithmus mitgenommen, daher liefert diese einen Output.

Hoffe das hat sich damit geklärt.

Gruß