The Programming and Proof System ATES (eBook, PDF)

Advanced Techniques Integration into Efficient Scientific Software
Redaktion: Puccetti, Armand

• Format: PDF

Produktbeschreibung

This ESPRIT project integrates formal proof techniques and abstraction mechanisms within a common framework to create an environment for scientific software design. It focuses upon recent developments concerning abstraction of data types, data base management, specification and program verification.

---

Dieser Download kann aus rechtlichen Gründen nur mit Rechnungsadresse in A, B, BG, CY, CZ, D, DK, EW, E, FIN, F, GR, HR, H, IRL, I, LT, L, LR, M, NL, PL, P, R, S, SLO, SK ausgeliefert werden.

Produktdetails

• Verlag: Springer Berlin Heidelberg
• Seitenzahl: 341
• Erscheinungstermin: 11. November 2013
• Englisch
• ISBN-13: 9783642845420
• Artikelnr.: 53155090

Inhaltsangabe

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.