The Programming and Proof System ATES
Advanced Techniques Integration into Efficient Scientific Software
1st Edition
Published on 11. November 2013
VIII, 341 pages
978-3-642-84542-0 (ISBN)
Description
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.
More details
Other editions
Additional editions
Armand Puccetti
The Programming and Proof System ATES
Advanced Techniques Integration into Efficient Scientific Software
Book
07/1991
Springer
€106.99
Shipment within 7-9 days
Persons
Max Afford (1906-1954) was an Australian playwright, radio producer, and mystery novelist. He gained recognition for his crime fiction, particularly for the Jeffrey Blackburn series, which featured a resourceful detective solving intricate mysteries. Afford was also a pioneer in Australian radio drama, producing popular shows during the golden age of radio. His contributions to both literature and broadcasting helped shape early Australian entertainment. Despite his relatively short life, Afford left a lasting legacy in Australian mystery fiction and radio storytelling.
Content
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.
