Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-26480
Titel: | A partial correctness logic for procedures (in an ALGOL-like language) |
VerfasserIn: | Sieber, Kurt |
Sprache: | Englisch |
Erscheinungsjahr: | 1984 |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | We extend Hoares logic by allowing quantifiers and other logical connectives to be used on the level of Hoare formulas. This leads to a logic in which partial correctness properties of procedures (and not only of statements) can be formulated adequately. In particular it is possible to argue about free procedures, i.e. procedures which are not bound by a declaration but only "specified" semantically. This property of our logic (and of the corresponding calculus) is important from both a practical and a theoretical point of view, namely: -Formal proofs of programs can be written in the style of stepwise refinement. -Procedures on parameter position can be handled adequately, so that some sophisticated programs can be verified, which are beyond the power of other calculi. The logic as well as the calculus are similar to Reynolds specification logic. But there are also some (essential) differences which will be pointed out in this paper. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291-scidok-52011 hdl:20.500.11880/26536 http://dx.doi.org/10.22028/D291-26480 |
Schriftenreihe: | Bericht / A / Fachbereich Angewandte Mathematik und Informatik, Universität des Saarlandes |
Band: | 1984/13 |
Datum des Eintrags: | 10-Apr-2013 |
Fakultät: | MI - Fakultät für Mathematik und Informatik |
Fachrichtung: | MI - Informatik |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
fb14_1984_13.pdf | 35,53 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.