Programming from Specifications

Programming from Specifications

Presents a rigorous treatment of most elementary program-development constructs, including iteration, recursion, procedures, parameters, modules and data refinement.

Publication date: 31 Dec 1998

ISBN-10: 0131232746

ISBN-13: n/a

Paperback: 322 pages

Views: 17,911

Type: N/A

Publisher: Prentice Hall

License: n/a

Post time: 26 Nov 2004 07:16:27

Programming from Specifications

Programming from Specifications Presents a rigorous treatment of most elementary program-development constructs, including iteration, recursion, procedures, parameters, modules and data refinement.
Tag(s): Formal Methods
Publication date: 31 Dec 1998
ISBN-10: 0131232746
ISBN-13: n/a
Paperback: 322 pages
Views: 17,911
Document Type: N/A
Publisher: Prentice Hall
License: n/a
Post time: 26 Nov 2004 07:16:27
Book excerpts:

This book teaches elementary programming in the style that specifications and code are all programs; that there is a refinement order between programs; and that there is a specially restricted sub­language called 'code' that allows programs written in it to be executed with 'no thought at all'. The thinking is necessary elsewhere, to find the code that refines a given specification.

The approach rests on the work of Dijkstra, Hoare, and Floyd; and the programming language is Dijkstra's guarded commands, extended with specification constructs. The language itself is pre­sented in the early chapters, and each of its constructs is characterised by the refinement laws that it satisfies. The effect on a computer is described informally, as an aid to the intuition.

Later chapters are split between case studies and more advanced programming techniques. Each case study treats a programming example from beginning to end, using the methods available at that point, and is well known rather than especially intricate. The more advanced programming techniques are procedures, recursion, recursive data structures, modules and finally state transformation (including data refinement).

The book is intended to be useful both to those learning to program and to those who --- programmers already --- would like to make the link between their existing skill and the specifications from which their programs (should) spring. Experience based on nearly 10 years' exposure to second­-year computing undergraduates sug­gests, however, that the best approach is at first to exercise a fairly light touch on the refinement laws. For beginning programmers they should assist, not prescribe: at that stage, the list of refinement laws is for reference, not for certification. And learning to use invariants for iterations is work enough on its own.

Light touch or no, the underlying theme of specification, refinement and code is one that students respond to, and it informs their approach to other courses and to computing generally. More experienced programmers may recognise some of those features in specification and development methods such as Z and VDM, for parts of which the refinement calculus forms an adjunct or even an alternative.




About The Author(s)


No information is available for this author.

Carroll Morgan

No information is available for this author.


Book Categories
Sponsors
Icons8, a free icon pack