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)
Verfasser: Sieber, Kurt
Sprache: Englisch
Erscheinungsjahr: 1984
DDC-Sachgruppe: 004 Informatik
Dokumentart : Report (Bericht)
Kurzfassung: 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
Schriftenreihe: Bericht / A / Fachbereich Angewandte Mathematik und Informatik, Universität des Saarlandes
Band: 1984/13
SciDok-Publikation: 10-Apr-2013
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
fb14_1984_13.pdf35,53 MBAdobe PDFÖffnen/Anzeigen

Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.