Zusammenfassung
Wir haben eine Sprache PASQUALE-L entworfen, mit der einige neuere Konzepte aus der theoretischen Informatik wie Programmverifikation und abstrakte Datentypen für lauffähige PASCAL-Programme verfügbar gemacht werden. Die Sprache ist in ein Verifikationssystem PASQUALE eingebettet, dessen Verification Condition Generator eine Implementierung der axiomatischen Definition von PASCAL ist. Die dort angegebene Verifikationsregel für Prozedur-Aufrufe wird mit Hilfe einer Transformationsregel realisiert.
PASQUALE-L erweitert PASCAL um ein Modulkonzept und um Sprachkonstrukte zur formalen Spezifikation von Programmen und Modulen. Ein PASQUALE-Modul besteht aus Funktionen und Prozeduren sowie internen Daten und ist auf der VAX unter VMS unabhängig übersetzbar. PASQUALE-L erlaubt so die Implementierung von abstrakten Datentypen in Modulen, die zu lauffähigen Programmen gebunden werden können.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Literaturverzeichnis
AdaTEC (Ed.): Reference Manual for the Ada Programming Language -Draft-. United States Department of Defense, July 1982
British Standards Institution: Specification for Computer Programming Language Pascal. BS 6192: 1982
The CIP Language Group: Report on A Wide Spectrum Language for Program Specification and Development. Technische Universität München, Institut für Informatik, TUM-18104, May 1981
Hoare,C. A. R.: An Axiomatic Basis for Computer Programming. Communications of the ACM, Vol 12 No 10 (1969), 576 - 583
Hoare,C. A. R. and Wirth,N.: An Axiomatic Definition of the Programming Language PASCAL, acta informatica 2, 335 - 355 (1973)
Hohlfeld,B.: Zur Verifikation von Funktionen und Prozeduren in PASCAL. AEG-TELEFUNKEN, Forschungsinstitut Ulm, Technischer Bericht Nr. 12.010/82
Hohlfeld,B.: Implementierung von abstrakten Datentypen in PASCAL-Programmen. AEG-TELEFUNKEN, Forschungsinstitut Ulm,
Technischer Bericht Nr. 12. 026/83
Hohlfeld,B.: Verifikationsregeln für eine PASCAL-Untermenge mit Modulkonzept. AEG-TELEFUNKEN, Forschungsinstitut Ulm,
Technischer Bericht Nr. 12. 050/83
Jensen,K. and Wirth,N.: PASCAL: User manual and report. Springer, New York 1975
Stanford PASCAL Verifier - User Manual. Computer Science Departement Stanford University 1979
VAX-11 PASCAL V1.2: Language Reference Manual. digital equipment corporation, Maynard, Massachusetts 1979
Wirth.N.: Programming in MODULA-2. Springer-Verlag, Berlin 1982
Wolter (ed): Höhere Programmiersprachen für Industrieroboter. Kernforschungszentrum Karlsruhe, KFK - PFT 51
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1984 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Hohlfeld, B. (1984). Programmverifikation in lauffähigen PASCAL-Programmen. In: Ammann, U. (eds) Programmiersprachen und Programmentwicklung. Informatik-Fachberichte, vol 77. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-69393-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-69393-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12905-9
Online ISBN: 978-3-642-69393-9
eBook Packages: Springer Book Archive