The programming and proof system ATES advanced techniques integration into efficient scientific software
General Material Designation
[Book]
First Statement of Responsibility
Armand Puccetti (ed.). With contrib. by D. Brocard ...
.PUBLICATION, DISTRIBUTION, ETC
Name of Publisher, Distributor, etc.
Berlin Springer Luxembourg Off. for Official Publ. of the European Communities
Date of Publication, Distribution, etc.
1991
PHYSICAL DESCRIPTION
Specific Material Designation and Extent of Item
(VIII, 341 Seiten, 4,77 MB)
SERIES
Series Title
EUR, 13548; Research reports ESPRIT; Project 1158, ATES
CONTENTS NOTE
Text of Note
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.1.1 The AFFIRM progamming environment.- 2.1.2 The GYPSY programming environment.- 2.1.3 The Stanford Pascal Verifier.- 2.1.4 The IOTA programming environment.- 2.1.5 The Alphard programming language.- 2.1.6 Summary.- 2.2 Proof systems.- 2.2.1 The LCF proof system.- 2.2.2 The Boyer-Moore theorem prover.- 2.2.3 The Illinois theorem prover.- 2.2.4 Plaisted's theorem prover.- 2.2.5 The SPADE proof system.- 2.2.6 Final remarks.- 2.3 Conclusions.- 2.4 References.- 3 The Programming Language.- 3.1 General presentation.- 3.1.1 Overview.- 3.1.2 Characteristic properties.- 3.1.3 Notations.- 3.2 Types and operators.- 3.2.1 Objects and types.- 3.2.2 Operator specification.- 3.2.3 Operator chapter.- 3.3 Constructions and algorithms.- 3.3.1 Abstract context.- 3.3.2 Constructions.- 3.3.3 Algorithms.- 3.3.4 Algorithm chapter.- 3.4 Structures and modules.- 3.4.1 Concrete context.- 3.4.2 Structures.- 3.4.3 Modules.- 3.4.4 Module chapter.- 3.5 Development with ATES.- 3.5.1 Books.- 3.5.2 Chapters.- 3.5.3 Actions on a book.- 3.5.4 Debugging.- 3.6 Advanced features.- 3.6.1 Genericity.- 3.6.2 Special operators.- 4 The Applications within the ATES Project.- 4.1 Introduction.- 4.2 The first application.- 4.2.1 Problem description.- 4.2.2 Formulation.- 4.2.3 The finite element method: theoretical overview.- 4.2.4 The finite element method: implementation overview.- 4.2.5 The F.E.M. model.- 4.2.6 Results validation.- 4.3 The second application.- 4.3.1 3-D extension of the library.- 4.3.2 3-D mesh generation.- 4.3.3 The Delaunay triangulation.- 4.3.4 Boundary conformity problems.- 4.3.5 General chart.- 4.3.6 Some applications.- 4.4 Performance considerations.- 4.4.1 Performances and ATES system.- 4.4.2 IO aspect.- 4.4.3 Memory aspect.- 4.4.4 CPU Aspect.- 4.4.5 CPU: A performance test.- 4.5 References.- 5 The Specification and Proof Language.- 5.1 Basic mathematical elements for proof.- 5.1.1 The sets.- 5.1.2 Functions and constants.- 5.1.3 Expressions and predicates.- 5.2 Axioms.- 5.2.1 Definition.- 5.2.2 Syntax.- 5.2.3 Example.- 5.3 Types and Operator specifications.- 5.3.1 Modeling types.- 5.3.2 Definingpre- and post-conditions foroperators.- 5.3.3 Specifying secondary variables.- 5.3.4 Specifications of system-generated operators.- 5.4 Proof elements.- 5.4.1 Loops and invariants.- 5.4.2 Syntax.- 5.4.3 Concrete models.- 5.4.4 Abstraction functions.- 5.4.5 Representation functions.- 6 Proving the Correctness of ATES Programs.- 6.1 Definition of the correctness.- 6.1.1 An operational semantics of ATES operators.- 6.1.2 A first order predicate logic.- 6.1.3 The predicate transformer WP.- 6.2 The interactive proof environment.- 6.2.1 Elements required for proofs.- 6.2.2 Predicate transformation and interactivity.- 6.2.3 The proof system's user interface.- 6.3 Proving the verification conditions.- 6.3.1 Introduction.- 6.3.2 The simplification methods.- 6.3.3 Relations with theorem proving.- 6.4 Example: the 1D heat transfer problem.- 6.4.1 Reading the input.- 6.4.2 Solving the discrete mathematical problem.- 6.4.3 Write result on output.- 6.4.4 The data-structures and their models.- 6.4.5 The actual proof.- 6.5 Conclusions.- 6.6 References.- 7 Extending the Techniques to Parallel Programs.- 7.1 Formal synthesis and verification of concurrent programs.- 7.1.1 Introduction.- 7.1.2 Parallelism within the sequential framework.- 7.1.3 Formal tools for nondeterministic concurrency.- 7.1.4 Development of a data transfer protocol.- 7.2 Validation of the approach in the real-time area.- 7.2.1 Objective.- 7.2.2 Ada features.- 7.2.3 Specifications and proofs.- 7.2.4 Related works.- 7.2.5 A short example.- 7.2.6 Specification and proof with LOTOS.- 7.2.7 Conclusion.- 7.3 References.- 8 Implementation Issues.- 8.1 Generalities.- 8.1.1 Some data about the system.- 8.1.2 Overview of the system organization.- 8.2 The ATES compiler.- 8.2.1 Initialisation.- 8.2.2 The parser.- 8.2.3 Semantic analysis of operators.- 8.2.4 Semantic analysis of algorithms.- 8.2.5 Semantic analysis of modules.- 8.2.6 Code generation.- 8.2.7 Code compilation and execution.- 8.3 The ATES proof system.- 8.3.1 Semantic analysis of axiom chapters.- 8.3.2 Semantic analysis of specification chapters.- 8.3.3 Semantic analysis of proof chapters.- 8.4 The ATES correctness proof system.- 8.4.1 The simplifier.- 8.4.2 The data manager.- 8.4.3 The graphic proof interface.- 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.
TOPICAL NAME USED AS SUBJECT
Automatic theorem proving.
Computer programming.
Computer software -- Development.
PERSONAL NAME - PRIMARY RESPONSIBILITY
Armand Puccetti (ed.). With contrib. by D. Brocard ...