The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

   [All my apologizes if you receive multiple copies of this message]

I'm pleased to announce that my book (with a nice foreword by G. Huet)

  Understanding Formal Methods 
  Springer
  ISBN 1-85233-247-6
  
is available.

Best wishes,
  Jean-Francois Monin

----------------------------------------------------------------------
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