ISSN:
1436-5057
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Description / Table of Contents:
Zusammenfassung Die vorliegende Arbeit analysiert die Erfahrungen, die bei der Durchführung formaler Korrektheitsbeweise an schon exsiterenden Programmen gemacht wurden. Mit Hilfe der Hoareschen Methode der Programmverfikation wurde der von an Emden angegebene Quicksort Algorithmus als richtig bewiesen. Dafür was es jedoch notwendig, eine Reihe von Veränderungen an dem Algorithmus vorzunehmen, um ihn an das Beweisverfahren und die existierenden Axiome anzupassen. Die gegenseitige Einflußnahme der Veränderungen und des Beweisverfahrens werden analysiert und Schlüse über die Verwendbarkeit des Hoareschen Verifikationsverfahrens für existierende Programme werden gezogen.
Notes:
Abstract Using the Quicksort Algortihm, given by van Emden, an analysis is made how Hoare's method of program verification can be applied to already existing programs. Changes to these programs become necessary to adopt them to the proving method and to the existing axioms. The interdependencies between these changes and the verification method are discussed and conclusions are draw about the applicability of Hoare's Methods for proving already existing programs.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF02244016
Permalink
