عنوان

The programming and proof system ATES advanced techniques integration into efficient scientific software

(Number (ISBN

0387541888

(Number (ISBN

3540541888

(Number (ISBN

9780387541884

(Number (ISBN

9783540541882

Number

b538783

Title Proper

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 ...

Name of Publisher, Distributor, etc.

Berlin Springer Luxembourg Off. for Official Publ. of the European Communities

Date of Publication, Distribution, etc.

1991

Specific Material Designation and Extent of Item

(VIII, 341 Seiten, 4,77 MB)

Series Title

EUR, 13548; Research reports ESPRIT; Project 1158, ATES

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.

Automatic theorem proving.

Computer programming.

Computer software -- Development.

Armand Puccetti (ed.). With contrib. by D. Brocard ...

Armand Puccetti

Didier Brocard

Europäische Kommission

Electronic name

[Book]

Y