The Programming and Proof System Ates: Advanced Techniques Integration Into Efficient Scientific Software

ISBN-13: 9783540541882 / Angielski / Miękka / 1991 / 341 str.

Armand Puccetti; D. Brocard; P. Gagert

Opis

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.

Spis treści

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.