عنوان

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

شابک

0387541888

شابک

3540541888

شابک

9780387541884

شابک

9783540541882

شماره

b538783

عنوان اصلي

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

نام عام مواد

[Book]

نام نخستين پديدآور

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

نام ناشر، پخش کننده و غيره

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

تاریخ نشرو بخش و غیره

1991

نام خاص و کميت اثر

(VIII, 341 Seiten, 4,77 MB)

عنوان فروست

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

متن يادداشت

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

نام الکترونيکي

نوع ماده

[Book]

تكميل شده

Y