Rigorous software development: an introduction to program verification

✍ Scribed by Almeida, José Bacelar;Frade, Maria João;Pinto, Jorge Sousa;Sousa, Simão Melo de

• Publisher: Springer
• Year: 2011
• Tongue: English
• Leaves: 269
• Series: Undergraduate topics in computer science
• Category: Library

✦ Synopsis

The use of mathematical methods in the development of software is essential when reliable systems are sought; in particular they are now strongly recommended by the official norms adopted in the production of critical software. Program Verification is the area of computer science that studies mathematical methods for checking that a program conforms to its specification. This text is a self-contained introduction to program verification using logic-based methods, presented in the broader context of formal methods for software engineering. The idea of specifying the behaviour of individual software components by attaching contracts to them is now a widely followed approach in program development, which has given rise notably to the development of a number of behavioural interface specification languages and program verification tools. A foundation for the static verification of programs based on contract-annotated routines is laid out in the book. These can be independently verified, which provides a modular approach to the verification of software. The text assumes only basic knowledge of standard mathematical concepts that should be familiar to any computer science student. It includes a self-contained introduction to propositional logic and first-order reasoning with theories, followed by a study of program verification that combines theoretical and practical aspects - from a program logic (a variant of Hoare logic for programs containing user-provided annotations) to the use of a realistic tool for the verification of C programs (annotated using the ACSL specification language), through the generation of verification conditions and the static verification of runtime errors.

✦ Table of Contents

Preface......Page 6
Acknowledgments......Page 8
Contents......Page 9
A Formal Approach to Software Engineering......Page 13
Test and Simulation-Based Reliability......Page 14
An Alternative Approach: Formal Methods......Page 15
Requirements: Functional, Security, and Safety......Page 16
Safety Critical System Standards......Page 17
The Common Criteria......Page 18
From Classic Software Engineering to Formal Software Engineering......Page 19
This Book......Page 23
References......Page 24
An Overview of Formal Methods Tools and Techniques......Page 26
Some Existing Formal Methods Taxonomies......Page 27
Specifying and Analysing......Page 28
Abstract State Machines......Page 29
Set and Category Theory......Page 30
Automata-Based Modelling......Page 31
Modelling Languages for Real-Time Systems......Page 32
Algebraic Specification......Page 35
Declarative Modelling......Page 36
Specifying and Proving......Page 37
Logic in a Nutshell......Page 38
Classical versus Intuitionistic Logic......Page 39
Temporal Logic......Page 40
Proof Assistants......Page 41
Model Checking......Page 42
Program Logics and Program Annotation......Page 43
Specifying and Deriving......Page 44
Refinement......Page 45
Specifying and Transforming......Page 47
Conclusions......Page 48
Are Formal Methods Tools Ready for Industry?......Page 49
To Learn More......Page 50
References......Page 51
Propositional Logic......Page 56
Syntax......Page 57
Semantics......Page 58
Proof System......Page 65
Soundness and Completeness......Page 72
Validity Checking: Semantic Methods......Page 75
Normal Forms in Propositional Logic......Page 76
Validity of CNF Formulas......Page 79
Satisfiability of CNF Formulas......Page 80
Validity Checking: Deductive Methods......Page 82
To Learn More......Page 85
Exercises......Page 87
References......Page 89
First-Order Logic......Page 91
Syntax......Page 92
Semantics......Page 97
Proof System......Page 105
Soundness and Completeness......Page 110
Negation and Prenex Normal Forms......Page 112
Herbrand/Skolem Normal Forms and Semi-Decidability......Page 114
Decidable Fragments......Page 118
First-Order Logic with Equality......Page 119
Many-Sorted First-Order Logic......Page 120
Second-Order Logic......Page 123
First-Order Theories......Page 125
Equality......Page 127
Natural Numbers......Page 128
Integers......Page 129
Arrays......Page 130
Combining Theories......Page 131
To Learn More......Page 132
Exercises......Page 134
References......Page 137
Hoare Logic......Page 139
Annotated While Programs......Page 140
Program Semantics......Page 141
The Whileint Programming Language......Page 144
Specifications and Hoare Triples......Page 146
Loop Invariants......Page 150
Hoare Calculus......Page 153
The Whilearray Programming Language......Page 158
A Rule of Hoare Logic for Array Assignment......Page 160
Adaptation......Page 161
To Learn More......Page 164
Exercises......Page 165
References......Page 167
Mechanising Hoare Logic......Page 168
The Weakest Precondition Strategy......Page 171
An Architecture for Program Verification......Page 176
Calculating the Weakest Precondition......Page 177
Putting It All Together......Page 179
Verification Conditions for Whilearray Programs......Page 181
Equality of Arrays......Page 185
To Learn More......Page 186
Exercises......Page 187
References......Page 188
Error Semantics and Safe Programs......Page 189
Whileint with Errors......Page 192
Safety-Sensitive Calculus and VCGen......Page 193
Safe Whileint Programs......Page 195
Bounded Arrays: The Whilearray[N] Language......Page 196
Safe Whilearray[N] Programs......Page 198
An Alternative Formalisation of Bounded Arrays......Page 200
Exercises......Page 201
References......Page 202
Procedures and Contracts......Page 203
Procedures and Recursion......Page 204
The Notation......Page 205
Recursive Procedures......Page 206
Procedure Calls in System Hg......Page 207
Contracts and Mutual Recursion......Page 208
Programming with Contracts......Page 210
Inference System for Parameterless Procedures......Page 211
Verification Conditions for Parameterless Procedures......Page 212
Frame Conditions......Page 214
Procedures with Parameters......Page 216
Parameters Passed by Value......Page 219
Parameters Passed by Reference......Page 223
Aliasing......Page 226
Return Values and Pure Functions......Page 228
Local Variables in Functions......Page 231
Exercises......Page 234
References......Page 235
Specifying C Programs......Page 236
Array-Based Programs......Page 237
Using Axiomatics......Page 238
Function Calls......Page 240
State Labels and Behaviours......Page 241
To Learn More......Page 245
References......Page 246
Verifying C Programs......Page 247
Safety Verification......Page 248
Arithmetic Overflow Safety......Page 249
Safety of Array Access......Page 250
Adding Loop Invariants......Page 251
Termination Checking and Loop Variants......Page 252
Safety of Function Calls......Page 253
Functional Correctness: Array Partitioning......Page 254
Functional Correctness: Multiset Preservation......Page 256
A Word of Caution......Page 257
Pointer Variables and Parameters Passed by Reference......Page 259
To Learn More......Page 260
References......Page 261
Index......Page 263