Please use this identifier to cite or link to this item: doi:10.22028/D291-26480
Title: A partial correctness logic for procedures (in an ALGOL-like language)
Author(s): Sieber, Kurt
Language: English
Year of Publication: 1984
DDC notations: 004 Computer science, internet
Publikation type: Report
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 to this record: urn:nbn:de:bsz:291-scidok-52011
Series name: Bericht / A / Fachbereich Angewandte Mathematik und Informatik, Universität des Saarlandes
Series volume: 1984/13
Date of registration: 10-Apr-2013
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
fb14_1984_13.pdf35,53 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.