Jean-Francois Monin
  Understanding Formal Methods 
  Springer
  ISBN 1-85233-247-6

  Foreword by G. Huet

Also available in french, see file book.bib in the same directory

----------------------------------------------------------------------
This book is intended to help the student or the engineer who wants an
introduction to formal techniques, as well as the practitioner who
wishes to broaden her or his knowledge of this subject.
It mainly aims at providing a synthetic view of the logical
foundations of such techniques, including set theory and type theory,
with an emphasis on intuitive ideas, so that it can also be considered
as a practical complement to classical introductory manuals to logic, 
and to books dedicated to particular formal methods.


Table of Contents

1.  Motivation						  1 
1.1 Some Industrial Applications			  2 
1.2 What Is a Formal Method?				  3 
1.3 From Software Engineering to Formal Methods	 	  4 
1.4 On Weaknesses of Formal Methods			  6 
1.5 A Survey of Formal Methods				  7 
1.6 Aim of this Book					 10 
1.7 How to Read this Book				 11 
1.8 Notes and Suggestions for Further Reading		 12 

2.  Introductory Exercise				 15 
2.1 Exposition						 15 
2.2 Sketch of a Formal Specification			 16 
2.3 Is There a Solution?				 18 
2.4 Program Development					 22 
2.5 Summary						 32 
2.6 Semantics						 33 
2.7 Notes and Suggestions for Further Reading		 33 

3.  A Presentation of Logical Tools			 35 
3.1 Some Applications of Logic				 36 
3.2 Antecedents						 39 
3.3 The Different Branches of Logic			 40 
3.4 Mathematical Reminders				 45 
3.5 Well-founded Relations and Ordinals			 51 
3.6 Fixed Points					 57 
3.7 More About Computability				 58 
3.8 Notes and Suggestions for Further Reading		 64 

4.  Hoare Logic						 65 
4.1 Introducing Assertions in Programs			 65 
4.2 Verification Using Hoare Logic			 66 
4.3 Program Calculus					 69 
4.4 Scope of These Techniques				 73 
4.5 Notes and Suggestions for Further Reading		 74
 
5.  Classical Logic					 75 
5.1 Propositional Logic					 75 
5.2 First-order Predicate Logic				 79 
5.3 Significant Examples				 84 
5.4 On Total Functions, Many-sorted Logics		 87 
5.5 Second-order and Higher-order Logics		 89 
5.6 Model Theory					 91 
5.7 Notes and Suggestions for Further Reading		 94 

6.  Set-theoretic Specifications			 95 
6.1 The Z Notation					 95 
6.2 VDM							102 
6.3 The B Method					105 
6.4 Notes and Suggestions for Further Reading		110 

7.  Set Theory						111 
7.1 Typical Features					111 
7.2 Zermelo--Fraenkel Axiomatic System			113 
7.3 Induction						117 
7.4 Sets, Abstract Data Types and Polymorphism		121 
7.5 Properties of ZF and ZFC				123 
7.6 Summary						123 
7.7 Notes and Suggestions for Further Reading		124 

8.  Behavioral Specifications				125 
8.1 Unity						125 
8.2 Transition Systems					129 
8.3 CCS, a Calculus of Communicating Systems		134 
8.4 The Synchronous Approach on Reactive Systems	136 
8.5 Temporal Logic					137 
8.6 TLA							144 
8.7 Verification Tools					146 
8.8 Notes and Suggestions for Further Reading		147 

9.  Deduction Systems					149 
9.1 Hilbert Systems					150 
9.2 Natural Deduction					152 
9.3 The Sequent Calculus				163 
9.4 Applications to Automated Theorem Proving		168 
9.5 Beyond First-order Logic				175 
9.6 Dijkstra--Scholten's System				176 
9.7 A Word About Rewriting Systems			181 
9.8 Results on Completeness and Decidability		182 
9.9 Notes and Suggestions for Further Reading		187 

10.  Abstract Data Types and Algebraic Specification	189 
10.1 Types						189 
10.2 Sets as Types					190 
10.3 Abstract Data Types				194 
10.4 Semantics						198 
10.5 Example of the Table				199 
10.6 Rewriting						200 
10.7 Notes and Suggestions for Further Reading		200 

11.  Type Systems and Constructive Logics		203 
11.1 Yet Another Concept of a Type			203 
11.2 The Lambda-calculus				204 
11.3 Intuitionistic Logic and Simple Typing		212 
11.4 Expressive Power of the Simply Typed $\lambda $-calculus
							218 
11.5 Second-Order Typing: System F			222 
11.6 Dependent Types					227 
11.7 Example: Defining Temporal Logic			230 
11.8 Towards Linear Logic				231 
11.9 Notes and Suggestions for Further Reading		232 

12.  Using Type Theory					233 
12.1 The Calculus of Inductive Constructions		234 
12.2 More on Type Theory				237 
12.3 A Program Correct by Construction			243 
12.4 On Undefined Expressions				251 
12.5 Other Proof Systems Based on Higher-order Logic	251 
12.6 Notes and Suggestions for Further Reading		253 

Bibliography						255 
Index							269