Geschäftskunden Kundenprogramme
Vor Ort
Merkzettel Warenkorb
  • Produktbild: The Programming and Proof System ATES
  • Produktbild: The Programming and Proof System ATES

The Programming and Proof System ATES Advanced Techniques Integration into Efficient Scientific Software

Aus der Reihe Research Reports Esprit

Fr. 137.00

inkl. gesetzl. MwSt., Versandkostenfrei

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

24.07.1991

Herausgeber

Armand Puccetti

Verlag

Springer Berlin

Seitenzahl

341

Maße (L/B/H)

24.4/17/2 cm

Gewicht

607 g

Auflage

1. Auflage

Sprache

Englisch

ISBN

978-3-540-54188-2

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

24.07.1991

Herausgeber

Armand Puccetti

Verlag

Springer Berlin

Seitenzahl

341

Maße (L/B/H)

24.4/17/2 cm

Gewicht

607 g

Auflage

1. Auflage

Sprache

Englisch

ISBN

978-3-540-54188-2

Herstelleradresse

Springer Heidelberg
Tiergartenstr. 17
69121 Heidelberg
DE
buchhandel-buch@springer.com

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)
  • Produktbild: The Programming and Proof System ATES
  • Produktbild: The Programming and Proof System 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.