Theory and Practice of Program Development

AvDerek J. Andrews

Häftad, Engelska, 1997

Del i serien Formal Approaches to Computing and Information Technology (FACIT)

573 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Fler format och utgåvor

E-bok

739 kr

Beskrivning

A Theory and Practice of Program Development provides a comprehensive introduction to a software development method based on VDM-SL. Each development step is rigorously justified, and the strategies and transformations used are justified and explained ma thematically. The approach provides the formal semantics of a simple, but powerful, wide-spectrum programming language and gives a formal definition of both algorithmic and data refinement. Unlike other texts, it covers both the theory and practice of program development. Although based on VDM-SL, no knowledge of this language is assumed, thus making it widely accessible. A Theory and Practice of Program Development is intended for 3rd/4th year undergraduate and postgraduate students taking formal methods and software engineering; software developers involved in the production of provably correct computer systems and reusa ble design and the problems of reusable code.

Produktinformation

Utgivningsdatum:1997-07-04
Mått:155 x 235 x 23 mm
Vikt:639 g
Format:Häftad
Språk:Engelska
Serie:Formal Approaches to Computing and Information Technology (FACIT)
Antal sidor:405
Upplaga:97001
Förlag:Springer-Verlag Berlin and Heidelberg GmbH & Co. KG
ISBN:9783540761624

Utforska kategorier

Databaser inom Data och IT
Programmeringsböcker inom Data och IT

Innehållsförteckning

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.4 Non-determinism and Partial Commands.- 2.5 The Concepts of Predicate Transformers.- 2.6 Substitution.- 2.7 The Formal Semantics of the Kernel Language.- 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.4 A Normal Form.- 3.5 Some Further Properties.- 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.4 Limits of Predicate Transformers.- 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.7 Summary.- 6. The Basic Commands.- 6.1 The Constant Commands.- 6.2 Assertions.- 6.3 Assignment.- 6.4 Summary.- 7. Declarations and Blocks.- 7.1 The Declaration Command.- 7.2 Some Interactions Between Commands.- 7.3 The Definitional Commands.- 7.4 Refining Definitional Commands.- 7.5 Defining Constant Values.- 7.6 Logical Constants.- 7.7 Summary.- 8. Command Sequences.- 8.1 Solve a Part and then the Whole.- 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 RefiningSpecifications.- 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.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.2 Logical Constants Revisited.- 12.3 Summary.- 13. On Refinement and Loops.- 13.1 The Factorial Problem.- 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.5 Summary.- 17. Data refinement.- 17.1 The Refinement Strategy.- 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.7 A Summary of the Approach.- 17.8 Summary.- 18. A Theory of Data Refinement.- 18.1 An Approach to Data Refinement.- 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.2Another Approach to the Refinement.- 19.3 Summary.- 20. Stacks and Queues.- 20.1 A Finite Stack.- 20.2 A stack of Boolean Values.- 20.3 A Finite Queue.- 20.4 An Efficient Queue.- 21. Dynamic Data Structures.- 21.1 Simulating a Linked List.- 21.2 Explicit Pointers.- 21.3 The Stack Using Explicit 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.

Mer från samma författare

Semantics of Specification Languages (SoSL)

C.A. Middelburg, Jan F. Groote, Derek J. Andrews

E-bok

2012

739 kr

Semantics of Specification Languages (SoSL)

Derek J. Andrews, Jan F. Groote, C.A. Middelburg

Häftad, 1994

573 kr

Mer från samma serie

Program Development by Refinement

Kaisa Sere, Emil Sekerinski, Emil Sekerinski, Kaisa Sere

Häftad, 1998

2 269 kr

Software Specification Methods

Marc Frappier, Henri Habrias

Häftad, 2000

1 138 kr

Specification Case Studies in RAISE

Hung Dang Van, Chris George, Tomasz Janowski, Richard Moore

Häftad, 2002

1 138 kr

Industrial-Strength Formal Methods in Practice

Michael G. Hinchey, Jonathan P. Bowen

Häftad, 1999

1 704 kr

Systems, Models and Measures

Agnes Kaposi, Margaret Myers

Häftad, 1993

573 kr

Proof in VDM: A Practitioner’s Guide

Juan C. Bicarregui, John Fitzgerald, Peter A. Lindsay, Richard Moore, Brian Ritchie

Häftad, 1993

556 kr

Notations for Software Design

Loe M.G. Feijs, Hans B.M. Jonkers, Cornelis A. Middelburg

Häftad, 1994

573 kr

On the Refinement Calculus

Carroll Morgan, Trevor Vickers

Häftad, 1994

573 kr

Formal Methods and Object Technology

Stephen J. Goldsack, Stuart J.H. Kent

Häftad, 1996

1 138 kr

Formal Object-Oriented Development

Kevin Lano

Häftad, 1995

573 kr

Du kanske också är intresserad av

Air-Breathing Fishes

Jeffrey B. Graham

E-bok

1997

1 403 kr