Geschäftskunden Kundenprogramme
Vor Ort
Merkzettel Warenkorb
A Theory and Practice of Program Development

A Theory and Practice of Program Development

Aus der Reihe

Fr. 72.90

inkl. gesetzl. MwSt.
Versandkostenfrei
Taschenbuch

Taschenbuch

Fr. 72.90 eBook

eBook

Fr. 62.90

A Theory and Practice of Program Development

Ebenfalls verfügbar als:

Taschenbuch

Taschenbuch

ab Fr. 72.90
eBook

eBook

ab Fr. 62.90

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

04.07.1997

Verlag

Springer Berlin

Seitenzahl

405

Maße (L/B/H)

23.5/15.5/2.2 cm

Beschreibung

Details

Einband

Taschenbuch

Erscheinungsdatum

04.07.1997

Verlag

Springer Berlin

Seitenzahl

405

Maße (L/B/H)

23.5/15.5/2.2 cm

Gewicht

639 g

Auflage

1st Edition

Sprache

Englisch

ISBN

978-3-540-76162-4

Weitere Bände von Formal Approaches to Computing and Information Technology (FACIT)

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Erste Bewertung verfassen

Unsere Kundinnen und Kunden meinen

0.0

0 Bewertungen filtern
  • A Theory and Practice of Program Development
  • 1. Writing Correct Programs.- 1.1 Satisfying Specifications.- 1.2 An Alternative Approach.- 1.3 Summary.- 2. A Small Programming Language.- 2.1 Satisfying Specifications.- 2.2 Specifications and Programs.- 2.3 The Semantics of Commands.- 2.3.1 Some Primitive Commands.- 2.3.2 A Basic Command.- 2.3.3 New Commands from Old — Operators.- 2.4 Non-determinism and Partial Commands.- 2.5 The Concepts of Predicate Transformers.- 2.6 Substitution.- 2.6.1 Rules for Substitution.- 2.7 The Formal Semantics of the Kernel Language.- 2.7.1 The Bounded Commands.- 2.7.2 The Unbounded Commands.- 2.8 The Weakest Liberal Pre-conditions, Termination, and Relations.- 2.9 Executable Programs.- 2.10 Summary.- 3. Concepts and Properties.- 3.1 More Commands.- 3.2 The Domain of a Command.- 3.3 Some Properties of Commands.- 3.3.1 Sequence.- 3.3.2 Bounded Non-deterministic Choice.- 3.3.3 Guarded Commands.- 3.3.4 Unbounded Non-deterministic Choice.- 3.3.5 Assertions.- 3.4 A Normal Form.- 3.5 Some Further Properties.- 3.5.1 Setting and Testing Variables.- 3.6 The Primitive Commands Revisited.- 3.7 Initial Values.- 3.8 A Compiler for the Small Language.- 3.9 Summary.- 4. Building New Commands from Old.- 4.1 Defining Commands.- 4.2 An Approach to Recursion.- 4.3 Sequences of Predicates and their Limit.- 4.3.1 A Skeptical Result.- 4.3.2 A Credulous Result.- 4.4 Limits of Predicate Transformers.- 4.4.1 The Two Approaches.- 4.5 Limits of Commands.- 4.6 Tidying the Loose Ends.- 4.7 Epilogue.- 5. Program Refinement.- 5.1 Stepwise Refinement.- 5.2 Replacing Specifications.- 5.3 Conventions.- 5.4 Refinement Classes.- 5.5 Alternative Views of Refinement.- 5.6 Other Refinement Relations.- 5.6.1 Weak Refinement.- 5.6.2 Partial Refinement.- 5.6.3 Full Refinement.- 5.6.4 Strong Refinement.- 5.6.5 Refinement by Simulation.- 5.7 Summary.- 6. The Basic Commands.- 6.1 The Constant Commands.- 6.2 Assertions.- 6.3 Assignment.- 6.3.1 Implementation Issues.- 6.4 Summary.- 7. Declarations and Blocks.- 7.1 The Declaration Command.- 7.2 Some Interactions Between Commands.- 7.3 The Definitional Commands.- 7.3.1 Declarations.- 7.3.2 The Let Command.- 7.3.3 The Def Command.- 7.3.4 The Def and Let Commands Compared.- 7.4 Refining Definitional Commands.- 7.5 Defining Constant Values.- 7.5.1 Refining Functions and Constants.- 7.6 Logical Constants.- 7.7 Summary.- 8. Command Sequences.- 8.1 Solve a Part and then the Whole.- 8.1.1 Choosing the First Step.- 8.1.2 Choosing the Second Step.- 8.1.3 Choosing Both Steps.- 8.2 Summary.- 9. The Alternative Command.- 9.1 Divide and Conquer.- 9.2 The Partition.- 9.3 Reassembly.- 9.4 Alternatives — The If Command.- 9.5 Refining Specifications.- 9.6 Summary.- 10. The Iterative Command.- 10.1 Another Approach.- 10.2 The Generalized Loop and Refinement.- 10.3 The General Variant Theorem.- 10.4 An Application.- 10.5 Loops.- 10.6 Iteration — The Do Command.- 10.7 Practical Do Commands.- 10.8 The Refinement of Loop Bodies.- 10.8.1 Decreasing Variants.- 10.8.2 Increasing Variants.- 10.9 Summary.- 11. Functions and Procedures.- 11.1 Proper Procedures and their Calls.- 11.2 Function Procedures and their Calls.- 11.3 Function Calls in Expressions.- 11.4 An Alternative Approach to Parameters and Arguments.- 11.5 Postscript.- 11.6 Summary.- 12. An Example of Refinement at Work.- 12.1 The Problem — Integer Multiplication.- 12.1.1 Getting Started.- 12.1.2 The Refinement Strategy Continued.- 12.1.3 The Next Step.- 12.2 Logical Constants Revisited.- 12.3 Summary.- 13. On Refinement and Loops.- 13.1 The Factorial Problem.- 13.1.1 The First Solution.- 13.1.2 A Second Solution.- 13.2 Finding Guards and Invariants.- 13.3 Identifying the Loop Type Incorrectly.- 14. Functions and Procedures in Refinement.- 14.1 Factorial.- 14.2 Multiply.- 14.3 Summary.- 15. Refinement and Performance.- 15.1 A Second Approach to Multiplication.- 15.2 Fast Division.- 15.3 Summary.- 16. Searching and Sorting.- 16.1 A Diversion — the Array Data Type.- 16.2 Linear Search.- 16.3 Binary Search.- 16.4 A Simple Sort Algorithm.- 16.4.1 The First Attempt.- 16.4.2 The Other Approach.- 16.5 Summary.- 17. Data refinement.- 17.1 The Refinement Strategy.- 17.1.1 The Problem.- 17.2 The Refinement to Executable Code.- 17.3 The Next Step.- 17.4 The Refinement of the Operations.- 17.5 The First Refinement Step.- 17.6 The Next Refinement Step.- 17.6.1 The check Operation.- 17.6.2 Putting it all Together.- 17.6.3 Further Development.- 17.6.4 The Final Step.- 17.7 A Summary of the Approach.- 17.8 Summary.- 18. A Theory of Data Refinement.- 18.1 An Approach to Data Refinement.- 18.1.1 The Data Refinement of Declarations.- 18.1.2 Refinement and Specifications.- 18.2 Data Refinement in Practice.- 18.3 Another View of Data Refinement.- 18.4 Functional Refinement.- 18.5 An Alternative Data Refinement of Assignments.- 18.6 Summary.- 19. An Alternative Refinement of the Security System.- 19.1 A Data Refinement.- 19.2 Another Approach to the Refinement.- 19.3 Summary.- 20. Stacks and Queues.- 20.1 A Finite Stack.- 20.1.1 The Refinement.- 20.1.2 Reorganizing the Operations.- 20.2 A stack of Boolean Values.- 20.2.1 Some Lemmas about the Representation.- 20.2.2 The empty-stack Operation.- 20.2.3 The push Operation.- 20.2.4 The pop Operation.- 20.2.5 The read Operation.- 20.2.6 The is-empty Operation.- 20.2.7 The is-full Operation.- 20.2.8 The Code.- 20.2.9 Some Lessons.- 20.3 A Finite Queue.- 20.3.1 A Refinement of the Queue.- 20.3.2 Some Theorems.- 20.3.3 The Operations Transformed.- 20.3.4 An Extension to the System.- 20.4 An Efficient Queue.- 20.4.1 Some Properties.- 20.4.2 Lessons.- 21. Dynamic Data Structures.- 21.1 Simulating a Linked List.- 21.1.1 Some Theorems.- 21.1.2 The Operations Transformed.- 21.2 Explicit Pointers.- 21.3 The Stack Using Explicit Pointers.- 21.3.1 Standard Stack Specification to Pointers.- 21.4 Summary.- 22. Binary Trees.- 22.1 The Specification.- 22.2 The Refinement.- 22.3 The Refinement of the in Operation.- 22.4 The Refinement of the insert Operation.- 22.5 The Refinement of the delete Operation.- 22.6 An In-order Traversal.- 22.7 Summary.- 23. Epilogue.- 23.1 An Approach to Loose Patterns and Functions.- A. Program Refinement Rules.- A.1 Replace Specification.- A.2 Assume Pre-condition in Post-condition.- A.3 Introduce Assignment.- A.4 Introduce Command-semicolon.- A.5 Introduce Semicolon-command.- A.6 Introduce Leading Assignment.- A.7 Introduce Following Assignment.- A.8 Introduce Alternatives.- A.9 Introduce Iteration.- A.10 Introduce Proper Procedure Body.- A.11 Introduce Proper Procedure Call.- A.12 Introduce Function Procedure Body.- A.13 Introduce Function Procedure Call.- A.14 Add Variable.- A.15 Realize Quantifier.- A.16 Remove Scope.- A.17 Expand Frame.- A.18 Contract Frame.- A.19 Introduce Logical Constant.- A.20 Remove Logical Constant.- A.21 Refine Block.- A.22 Introduce Skip.