Korrektheit: Difference between revisions
No edit summary |
No edit summary |
||
| Line 2: | Line 2: | ||
Ergänzend zum Beispiel der Hoare-Logic, die benutzt wurde um praxisorientiert mitn der formale Methoden zu arbeiten, ein kurzer Verweis auf die benutzte Quelle : " An Axiomatic Basis for Computer Programming" , C.A.R. Hoave; Comm ACM 1969[http://www.cs.ucsb.edu/~kemm/courses/cs266/hoare69.pdf] | Ergänzend zum Beispiel der Hoare-Logic, die benutzt wurde um praxisorientiert mitn der formale Methoden zu arbeiten, ein kurzer Verweis auf die benutzte Quelle : " An Axiomatic Basis for Computer Programming" , C.A.R. Hoave; Comm ACM 1969[http://www.cs.ucsb.edu/~kemm/courses/cs266/hoare69.pdf] | ||
Software- Test | |||
Dijkstra [http://de.wikipedia.org/wiki/Edsger_Wybe_Dijkstra]ließ eimal das Zitat verlauten : " Tests können nie die Abwesenheit von Fehlern beweisen [Anwesenheit schon]" | |||
Nach solch einer Aussage stellt sich die Frage ob es sich überhaupt lohnt, mit dem Testverfahren die Korrektheit eines Algorithmus zu zeigen. Es erscheint einem doch plausibler sich auf die "formalen Methoden" zu berufen , mit dem Wissen, dass diese uns tatsächlich einen Beweis liefern können ob nun H oder nicht H gilt. | |||
Revision as of 10:38, 25 April 2008
24.April ( erst nur ein formales Skelett, Feinarbeit folgt noch)
Ergänzend zum Beispiel der Hoare-Logic, die benutzt wurde um praxisorientiert mitn der formale Methoden zu arbeiten, ein kurzer Verweis auf die benutzte Quelle : " An Axiomatic Basis for Computer Programming" , C.A.R. Hoave; Comm ACM 1969[1]
Software- Test
Dijkstra [2]ließ eimal das Zitat verlauten : " Tests können nie die Abwesenheit von Fehlern beweisen [Anwesenheit schon]"
Nach solch einer Aussage stellt sich die Frage ob es sich überhaupt lohnt, mit dem Testverfahren die Korrektheit eines Algorithmus zu zeigen. Es erscheint einem doch plausibler sich auf die "formalen Methoden" zu berufen , mit dem Wissen, dass diese uns tatsächlich einen Beweis liefern können ob nun H oder nicht H gilt.
