Blick ins Buch

The Programming and Proof System ATES

Advanced Techniques Integration into Efficient Scientific Software

Armand Puccetti (Herausgeber)

Buch | Softcover

VIII, 341 Seiten

1991
Springer Berlin (Verlag)
978-3-540-54188-2 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)

Artikel merken

Today, people use a large number of "systems" ranging in complexity from washing machines to international airline reservation systems. Computers are used in nearly all such systems: accuracy and security are becoming increasingly essential. The design of such computer systems should make use of development methods as systematic as those used in other engineering disciplines. A systematic development method must provide a way of writing specifications which are both precise and concise; it must also supply a way of relating design to specification. A concise specification can be achieved by restricting attention to what a system has to do: all considerations of implementation details are postponed. With computer systems, this is done by: 1) building an abstract model of the system -operations being specified by pre-and post-conditions; 2) defining languages by mapping program texts onto some collection of objects modelizing the concepts of the system to be dealt with, whose meaning is understood; 3) defining complex data objects in terms of abstractions known from mathematics. This last topic, the use of abstract data types, pervades all work on specifications and is necessary in order to apply ideas to systems of significant complexity. The use of mathematics based notations is the best way to achieve precision. 1.1 ABSTRACT DATA TYPES, PROOF TECHNIQUES From a practical point of view, a solution to these three problems consists to introduce abstract data types in the programming languages, and to consider formal proof methods.

1 Introduction.- 1.1 Abstract data types, Proof techniques.- 1.2 Motivation.- 1.3 Organization of the book.- 1.4 Acknowledgements.- 2 State of the Art.- 2.1 Abstract specification and programming languages.- 2.2 Proof systems.- 2.3 Conclusions.- 2.4 References.- 3 The Programming Language.- 3.1 General presentation.- 3.2 Types and operators.- 3.3 Constructions and algorithms.- 3.4 Structures and modules.- 3.5 Development with ATES.- 3.6 Advanced features.- 4 The Applications within the ATES Project.- 4.1 Introduction.- 4.2 The first application.- 4.3 The second application.- 4.4 Performance considerations.- 4.5 References.- 5 The Specification and Proof Language.- 5.1 Basic mathematical elements for proof.- 5.2 Axioms.- 5.3 Types and Operator specifications.- 5.4 Proof elements.- 6 Proving the Correctness of ATES Programs.- 6.1 Definition of the correctness.- 6.2 The interactive proof environment.- 6.3 Proving the verification conditions.- 6.4 Example: the 1D heat transfer problem.- 6.5 Conclusions.- 6.6 References.- 7 Extending the Techniques to Parallel Programs.- 7.1 Formal synthesis and verification of concurrent programs.- 7.2 Validation of the approach in the real-time area.- 7.3 References.- 8 Implementation Issues.- 8.1 Generalities.- 8.2 The ATES compiler.- 8.3 The ATES proof system.- 8.4 The ATES correctness proof system.- 8.5 References.- 9 Conclusion.- Appendix A. Formal Specification of the 1D Heat Transfer Problem.- Appendix B. Grammar of the ATES Specification Language.- Appendix C. Grammar of the ATES Source Language.

Erscheint lt. Verlag	24.7.1991
Reihe/Serie	Project 1158. ATES
Reihe/Serie	Research Reports Esprit
Co-Autor	D. Brocard, P. Gagert, P. Gribomont, O. Pirotte, A. Pucetti, J. Raguideau, A. Remouchamps, E. Ten Cate
Zusatzinfo	VIII, 341 p. 15 illus.
Verlagsort	Berlin
Sprache	englisch
Maße	170 x 244 mm
Gewicht	607 g
Themenwelt	Mathematik / Informatik ► Informatik ► Software Entwicklung
Schlagworte	Abstract Data Types • Abstrakte Datentypen • algorithms • Automatisches Beweisen • Datentyp • Design • Development • Finite Element Method • Formale Spezifikation • formal specification • Formal Specifications • language • Model • Modeling • programming • Programming language • Programmverifikation • Program verification • Semantics • Software • Software engineering • Software-Engineering • Software Engineering / Softwareentwicklung • Softwareentwicklung • theorem proving • verification
ISBN-10	3-540-54188-8 / 3540541888
ISBN-13	978-3-540-54188-2 / 9783540541882
Zustand	Neuware