Theorietestat 4: Korrektheitsbeweis SumMatrix

Cem
Neuling
Neuling
Beiträge: 3
Registriert: 16. Apr 2015 16:14

Theorietestat 4: Korrektheitsbeweis SumMatrix

Beitrag von Cem » 27. Jun 2017 21:11

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?

invariant
Mausschubser
Mausschubser
Beiträge: 65
Registriert: 6. Mai 2017 19:01

Re: Theorietestat 4: Korrektheitsbeweis SumMatrix

Beitrag von invariant » 27. Jun 2017 21:46

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ß

Antworten

Zurück zu „Archiv“