Please use this identifier to cite or link to this item: http://dx.doi.org/10.18419/opus-8913
Authors: Plödereder, Erhard
Title: A semantic model for the analysis and verification of programs in general, higher-level languages
Issue Date: 1980
Publisher: Cambridge, Mass. : Center for Research in Computing Technology
metadata.ubs.publikation.typ: Arbeitspapier
metadata.ubs.publikation.seiten: 1 Band (verschiedene Seitenzählungen)
Series/Report no.: TR / Center for Research in Computing Technology, Harvard University;1980,2
URI: http://elib.uni-stuttgart.de/handle/11682/8930
http://nbn-resolving.de/urn:nbn:de:bsz:93-opus-ds-89303
http://dx.doi.org/10.18419/opus-8913
metadata.ubs.bemerkung.extern: Zugl.: Harvard, Harvard University, Ph.D. thesis, 1980
Abstract: Today the predominant theoretical basis for the semantic analysis of programs is the inductive assertion method due to floyd 'Floyd1', and the deductive logical systems subsequently developed by Hoare and others. Howoever, these systems link the derivation of knowledge about programs directly to the verification of asserted programs; they do not provide an adequate basis for such tasks as source-to-source optimization, interactive program documentation, or static performance analysis. In varying degrees, they require the user to provide redundant specificatlons trlvially derivable from the program text. Furthermore,several features found in hlgher-level programming languages create substantial problems for the practical application of these deductive systems.
Appears in Collections:15 Fakultätsübergreifend / Sonstige Einrichtung

Files in This Item:
File Description SizeFormat 
ploe1.pdf74,92 MBAdobe PDFView/Open


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