Specifying Software (A Hands-On Introduction)

Provides an innovative hands-on introduction to techniques for specifying the behaviour of software components. It is primarily intended for use as a text book for a course in the 2nd or 3rd year of Computer Science and Computer Engineering programs, but it is also suitable for self-study. Using this book will help the reader improve programming skills and gain a sound foundation and motivation for subsequent courses in advanced algorithms and data structures, software design, formal methods, compilers, programming languages, and theory. The presentation is based on numerous examples and case studies appropriate to the level of programming expertise of the intended readership. The main topics covered are techniques for using programmer-friendly assertional notations to specify, develop, and verify small but non-trivial algorithms and data representations, and the use of state diagrams, grammars, and regular expressions to specify and develop recognizers for formal languages. Cover......Page __sk_0000.djvu Copyright......Page __sk_0004.djvu Contents......Page __sk_0005.djvu Preface......Page __sk_0009.djvu Introduction......Page __sk_0013.djvu A Algorithms......Page __sk_0023.djvu Introduction to Part A......Page __sk_0025.djvu 1.1 Case Study: Searching an Array......Page __sk_0027.djvu 1.2 Declarative Interface for Array Search......Page __sk_0030.djvu 1.3 Assertions......Page __sk_0031.djvu 1.4 Completing the Specification for Array Search......Page __sk_0037.djvu 1.5 Correctness of Code......Page __sk_0039.djvu 1.6 Additional Reading......Page __sk_0041.djvu 2.1 Some Programs for Array Searching......Page __sk_0043.djvu 2.2 Correctness Statements......Page __sk_0047.djvu 2.3 Simple Assignment Statements......Page __sk_0048.djvu 2.4 Substitution into Assertions......Page __sk_0050.djvu 2.5 Using Mathematical Facts......Page __sk_0052.djvu 2.6 Formal Proofs and Proof Tableaux......Page __sk_0054.djvu 2.7 Sequencing......Page __sk_0055.djvu 2.8 If Statements......Page __sk_0058.djvu 2.9 While Statements......Page __sk_0061.djvu 2.10 Termination of Loops......Page __sk_0065.djvu 2.11 Local Variables......Page __sk_0067.djvu 2.12 Discussion......Page __sk_0069.djvu 2.13 Additional Reading......Page __sk_0070.djvu 3.1 Searching an Array......Page __sk_0073.djvu 3.2 Minimal Entry of an Array......Page __sk_0077.djvu 3.3 Powers......Page __sk_0079.djvu 3.4 Division......Page __sk_0081.djvu 3.5 Binary Search in a Sorted Array......Page __sk_0083.djvu 3.6 The Number of Distinct Values in an Array......Page __sk_0088.djvu 3.7 Additional Reading......Page __sk_0091.djvu 4.1 For Loops......Page __sk_0093.djvu 4.2 Array-Component Assignment Statements......Page __sk_0095.djvu 4.3 Do-While Loops......Page __sk_0100.djvu 4.4 Sorting an Array......Page __sk_0103.djvu 4.5 Combining Correctness Statements......Page __sk_0111.djvu 4.6 Additional Exercises......Page __sk_0114.djvu 4.7 Additional Reading......Page __sk_0117.djvu B Data Representations......Page __sk_0119.djvu Introduction to Part B......Page __sk_0121.djvu 5.1 Informal Specification......Page __sk_0123.djvu 5.2 Formal Specification......Page __sk_0125.djvu 5.3 A Simple Implementation......Page __sk_0126.djvu 5.4 Program Organization......Page __sk_0128.djvu 5.5 Verification of a Data Representation......Page __sk_0131.djvu 5.6 A Caching Implementation......Page __sk_0134.djvu 5.7 Additional Reading......Page __sk_0136.djvu 6.1 Traversing a Sparse Set......Page __sk_0137.djvu 6.2 Sparse Arrays......Page __sk_0143.djvu 6.3 Sequences......Page __sk_0148.djvu 6.4 Bit-String Representation of Sets......Page __sk_0150.djvu 6.5 Reachability in a Directed Graph......Page __sk_0155.djvu 6.6 Sorting a Partially Ordered Set......Page __sk_0158.djvu 6.7 Additional Reading......Page __sk_0164.djvu C Language Recognizers......Page __sk_0167.djvu Introduction to Part C......Page __sk_0169.djvu 7.1 Strings......Page __sk_0171.djvu 7.2 Formal Languages......Page __sk_0172.djvu 7.3 Basic Operations on Languages......Page __sk_0174.djvu 7.4 Classes of Languages......Page __sk_0179.djvu 7.5 Additional Reading......Page __sk_0180.djvu 8.1 Basic Definitions......Page __sk_0181.djvu 8.2 Software Realization......Page __sk_0184.djvu 8.3 N ondeterminism......Page __sk_0188.djvu 8.4 State-Transition Diagrams with ε Transitions......Page __sk_0195.djvu 8.5 Reactive Systems......Page __sk_0196.djvu 8.6 Additional Reading......Page __sk_0201.djvu 9.1 From Regular Expressions to State Diagrams......Page __sk_0203.djvu 9.2 From State Diagrams to Regular Expressions......Page __sk_0208.djvu 9.3 Additional Operations on Regular Languages......Page __sk_0211.djvu 9.4 Nonregular Languages......Page __sk_0212.djvu 9.5 Other Formalisms......Page __sk_0216.djvu 9.6 Additional Reading......Page __sk_0217.djvu 10.1 Backus-Naur Formalism......Page __sk_0219.djvu 10.2 Derivations......Page __sk_0222.djvu 10.4 Ambiguity......Page __sk_0224.djvu 10.5 Push-Down Automata......Page __sk_0228.djvu 10.6 Non-Context-Free Languages......Page __sk_0232.djvu 10.7 Other Formalisms......Page __sk_0235.djvu 10.8 Additional Reading......Page __sk_0236.djvu 11.1 General Methods......Page __sk_0239.djvu 11.3 Recursive Descent......Page __sk_0240.djvu 11.4 Additional Reading......Page __sk_0253.djvu D Unimplementable Specifications......Page __sk_0255.djvu Introduction to Part D......Page __sk_0257.djvu 12.1 The Halting Problem......Page __sk_0259.djvu 12.2 The Church-Turing Thesis......Page __sk_0261.djvu 12.3 Unsolvability by Reduction......Page __sk_0262.djvu 12.4 Additional Reading......Page __sk_0264.djvu Appendices......Page __sk_0267.djvu A.1 Lexical Conventions......Page __sk_0269.djvu A.2 Basic Types and Constants......Page __sk_0271.djvu A.4 Variable Declarations......Page __sk_0273.djvu A.6 Expressions......Page __sk_0274.djvu A.7 Some Library Functions......Page __sk_0276.djvu A.8 Statements......Page __sk_0278.djvu A.9 Function Definitions......Page __sk_0281.djvu A.10 More Library Functions......Page __sk_0282.djvu A.13 Grammar......Page __sk_0285.djvu A.14 Additional Reading......Page __sk_0290.djvu B Hints for Selected Exercises......Page __sk_0291.djvu Index......Page __sk_0297.djvu This innovative volume provides a hands-on introduction to techniques for specifying the behavior of software components. A text for a second-year undergraduate course in Computer Science and Computer Engineering programs, it is also suitable for self-study. This book will help students to improve their programming skills and gain a sound foundation and motivation for subsequent courses in advanced algorithms and data structures, software design, formal methods, compilers, programming languages, and theory. The main topics covered are techniques for using programmer-friendly assertional notations to specify, develop, and verify small but non-trivial algorithms and data representations, and the use of state diagrams, grammars, and regular expressions to specify and develop recognizers for formal languages. The presentation is based on numerous examples and case studies appropriate to the level of programming expertise of the intended readership.

an Innovative Hands-on Introduction To Techniques For Specifying The Behaviour Of Software Components.

booknews

this Books Offers A Hands-on Introduction To Techniques For Specifying The Behavior Of Software Components. Presentation Is Based On Numerous Examples And Case Studies, With Descriptions Of Techniques For Using Programmer-friendly Assertional Notations To Specify, Develop, And Verify Small But Nontrivial Algorithms And Data Representations And For Using State Diagrams, Grammars, And Regular Expressions To Specify And Develop Recognizers For Formal Languages. The Book Is Appropriate For Second- And Third-year Computer Science And Computer Engineering Students Familiar With Basic Concepts Of Discrete Mathematics And Logic. Tennent Teaches Computing And Information Science At Queen's University, Canada. Annotation C. Book News, Inc., Portland, Or (booknews.com)