Structure Programming, Theory and Practice

COVER
FOREWORD
PREFACE
	The mathematical character of software
	Mental weight lifting
	About this book
	To the reader
	Acknowledgements
CONTENTS
CHAPTER 1 PRECISION PROGRAMMING
	1.1 Programming in the Small
		1.1.1 How to Write Correct Programs and Know It
		1.1.2 What Is a Correct Program?
		1.1.3 Proofs of Program Correctness
		1.1.4 An Intuitive Approach to Program Correctness
	1.2 Programming in the Large
		1.2.1 Conceptual Integrity
		1.2.2 The Difference Between Heuristics and Rigor
		1.2.3 Structured Programsand Good Design
		1.2.4 The Difference Between Detailing and Desig
		1.2.5 Design Validation by Top-Down Development
		1.2.6 The Basis for Software Reliability Is Design, Not Testing
CHAPTER 2 ELEMENTS OF LOGICAL EXPRESSION 1
	2.1 Overview
	2.2 Good English
		2.2.1 Structure and Content
		2.2.2 The Context of Communication
		2.2.3 Models of Communication
	2.3 Formal Logic
		2.3.1 Logical Propositions
		2.3.2 The Propositional Calculus
		2.3.3 The Predicate Calculus
	2.4 Sets and Functions
		2.4.1 Sets
		2.4.2 Relations
		2.4.3 Functions
		2.4.4 Recursive Functions
		2.4.5 Digraphs
		2.4.6 State Machines
	2.5 Lists and Strings
		2.5.1 List Structures
		2.5.2 Strings and Languages
		2.5.3 Formal Grammars
		2.5.4 Regular Expressions
	2.6 Related Reading
CHAPTER 3 ELEMENTS OF PROGRAM EXPRESSION
	3.1 Overview
	3.2 Process Design Language
		3.2.1 The Idea of PDL
		3.2.2 Outer Syntax and Inner Syntax in PDL
		3.2.3 Data Assignment in PDL 4
	3.3 Outer Syntax Control Structures
		3.3.1 Sequence Structures
		3.3.3 Iteration Structures
		3.3.4 Comments
		3.3.5 Expanding and Parsing PDL Control Structures
	3.4 Outer Syntax Data Structures
		3.4.1 Structures of Named Data
		3.4.2 Structures of Anonymous Data
			Stack
			Queue
			Sequence
		3.4.3 Sequence Extensions
		3.4.4 Set Extensions
		3.4.5 Data Spaces
	3.5 Outer Syntax System Structures
		3.5.1 Jobs and Procedures
		3.5.2 Systems and Modules
	3.6 Inner Syntax
		3.6.1 Inner Syntax Expressions
		3.6.2 Data Types
CHAPTER 4 STRUCTURED PROGRAMS
	4.1 Overview
	4.2 Program Execution
		4.2.1 Flowchart Programs
		4.2.2 Proper Programs
		4.2.3 Execution Charts and Trees
		Exercises
	4.3 Program Functions
		4.3.1 Data Assignment
		4.3.2 Program Effects on Data
		4.3.3 Program Equivalence
		Exercises
	4.4 Program Structures
		4.4.1 Prime Programs
		4 4.2 Compound Programs
		4.4.3 The Structure Theorem
		4.4.4 Recursion Structure Programs
		Exercises
	4.5 A Case Study in Program Structuring
		4.5.1 Prime Program Parsing
		4.5.2 An Improved Structuring Technique
		Exercises
CHAPTER 5 READING STRUCTURED PROGRAMS
	5.1 Overview
	5.2 Reading Fundamentals
		5.2.1 The Idea of Program Reading
		5.2.2 The Algebra of Structured Programs
		5.2.3 Reading Prime Programs
		5.2.4 Reading by Stepwise Abstraction
		Exercises
	5.3 Logical Commentary in Structured Programs
		5.3.1 The Structure of Logical Commentary
		5.3.2 Logical Commentary in Stepwise Abstraction
		Exercises
	5.4 A Case Study in Program Reading
		5.4.1 The Singsort Program
		5.4.2 The Prime Program Parse of Singsort
		5.4.3 Singsort in PDL
		5.4.4 Reading and Commenting Singsort
		5.4.5 A Segment Structured Singsort
		5.4.6 Open Questions
		5.4.7 A Stack Oriented Singsort
		Exercises
CHAPTER 6 THE CORRECTNESS OF STRUCTURED PROGRAMS
	6.1 Overview
	6.2 Verifying Structured Programs
		6 2.1 Verifying Correctness in Reading. Writing, and Validation
		6.2.2 The Algebra of Correctness of Structured Programs
		Exercises
	6.3 The Correctness of Prime Programs
		6.3.1 Program Termination
		6.3.2 The Iteration Recursion Lemma
		6.3.3 The Correctness Theorem
		6.3.4 Working Questions for Complete Correctness
		6.3.5 Correctness Proof Syntax
		Exercises
	6.4 Techniques for Proving Program Correctness
		6.4.1 Trace Tables
		6.4.2 Disjoint Rules
		6.4.3 Case-Structured Trace Tables
		6.4.4 Verifying Fordo Programs
		6.4.5 Direct Assertions about Program Functions
		Exercises
	6.5 Examples of Program Verification
		6.5.1 Proofs of PDL Primes With Scalar Data
		6.5.2 Proofs With Array Data
		6.5.3 Proofs with Anonymous Data
		6.5.4 Proofs of Larger Loop-Free Primes
		Exercises
	6.6 Loop Invariants in Correctness Proofs
		6.6.1 Loop Invariants
		6.6.2 The Invariant Status Theorem
		6.6.3 Full Invariants and Limited Invariants
		Exercises
	6.7 Formulas for Correct Structured Programs
		6.7.1 The Function Equations of Structured Programs
		6.7.2 The Ifthenelse Formula
		6.7.3 The Sequence Formula
		6.7.4 The Whiledo Formula
		Exercises
CHAPTER 7 WRITING STRUCTURED PROGRAMS
	7.1 Overview
	7.2 Writing Fundamentals
		7.2.1 Inventing Structured Programs
		7.2.2 The Discipline of Function Expansion
		7.2.3 Using Program Verification in Program Design
		7.2.4 Logical Commentary in Program Writing
		Exercises
	7.3 Programming Strategies
		7.3.1 Programming by Stepwise Refinement
		7.3.2 Case Study: Air Pollution
		7.3.3 Top-Down Structured Programming
		7.3.4 Programming by Stepwise Reorganization
		7.3.5 Case Study: World Capitals
		Exercises
	7.4 A Case Study in Detailing and Design: Long Division
		7.4.1 Detailing Versus Design
		7.4.2 A Long-Division Problem
		7.4.3 Detailing through Direct Experience
		7.4.4 Design through Stepwise Refinement
	7.5 A Case Study in Heuristics and Rigor: Making Change
		7.5.1 Heuristics Versus Rigor
		7.5.2 A Change-Making Problem
		7.5.3 A Heuristic Approach and Its Difficulties
		7.5.4 A Rigorous Solution and Its Expansion
		7.5.5 Redefining the Problem
	7.6 Another Case Study in Heuristics and Rigor: Tic Tac Toe
		7.6.1 Tic-Tac-Toe
		7.6.2 A Direct Approach
		7.6.3 A Heuristic Approach
		7.6.4 A Rigorous Design for Tic-Tac-Toe
		Exercises
INDEX