HOME > Detail View

Detail View

Understanding formal methods

Understanding formal methods (Loan 2 times)

Material type
단행본
Personal Author
Monin, Jean Francois, 1960- Hinchey, Michael G. (Michael Gerard) , 1969-
Title Statement
Understanding formal methods / written and translated by Jean Francois Monin ; translation editor, Michael G. Hinchey.
Publication, Distribution, etc
London ;   New York :   Springer,   c2003.  
Physical Medium
xv, 275 p. ; 24 cm.
ISBN
1852332476 (alk. paper)
General Note
"... published with the help of the French Ministere de la culture--Centre national du livre."  
Bibliography, Etc. Note
Includes bibliographical references (p. [255]-267) and index.
Subject Added Entry-Topical Term
Formal methods (Computer science)
000 01160camuu22003014a 4500
001 000000884134
005 20040614145848
008 020826s2003 enk b 001 0 engx
010 ▼a 2002030646
020 ▼a 1852332476 (alk. paper)
035 ▼a KRIC08999772
040 ▼a DLC ▼c DLC ▼d HYUC ▼d 211062 ▼d 211009
041 1 ▼a eng ▼h fre
042 ▼a pcc
049 1 ▼l 121095335 ▼f 과학
050 0 0 ▼a QA76.6 ▼b .M6513 2003
082 0 0 ▼a 004/.01/51 ▼2 21
090 ▼a 004.0151 ▼b M744u
100 1 ▼a Monin, Jean Francois, ▼d 1960-
240 1 0 ▼a Introduction aux methodes formelles. ▼l English
245 1 0 ▼a Understanding formal methods / ▼c written and translated by Jean Francois Monin ; translation editor, Michael G. Hinchey.
260 ▼a London ; ▼a New York : ▼b Springer, ▼c c2003.
300 ▼a xv, 275 p. ; ▼c 24 cm.
500 ▼a "... published with the help of the French Ministere de la culture--Centre national du livre."
504 ▼a Includes bibliographical references (p. [255]-267) and index.
650 0 ▼a Formal methods (Computer science)
700 1 ▼a Hinchey, Michael G. ▼q (Michael Gerard) , ▼d 1969-

Holdings Information

No. Location Call Number Accession No. Availability Due Date Make a Reservation Service
No. 1 Location Science & Engineering Library/Sci-Info(Stacks2)/ Call Number 004.0151 M744u Accession No. 121095335 Availability Available Due Date Make a Reservation Service B M

Contents information

Table of Contents

1. Motivation.- 1.1 Some Industrial Applications.- 1.1.1 Specification for Re-engineering.- 1.1.2 Proving Critical Railway Software.- 1.2 What Is a Formal Method?.- 1.3 From Software Engineering to Formal Methods.- 1.3.1 Towards More Rigorous Processes.- 1.3.2 Software Development Using Formal Methods.- 1.3.3 Formal Methods for the Customer.- 1.4 On Weaknesses of Formal Methods.- 1.5 A Survey of Formal Methods.- 1.5.1 Specialized and General Approaches.- 1.5.2 Emphasizing the Specification or the Verification.- 1.6 Aim of this Book.- 1.7 How to Read this Book.- 1.8 Notes and Suggestions for Further Reading.- 2. Introductory Exercise.- 2.1 Exposition.- 2.2 Sketch of a Formal Specification.- 2.3 Is There a Solution?.- 2.3.1 Doing Nothing.- 2.3.2 Attempting the Impossible.- 2.3.3 Weakening the Postcondition.- 2.3.4 Intermezzo: Sum of Sets.- 2.3.5 Strengthening the Precondition.- 2.4 Program Development.- 2.4.1 Prelude: Correctness of a Loop.- 2.4.2 Linear Search.- 2.4.3 Discussion: Reasoning Figures.- 2.4.4 Bounded Linear Search.- 2.4.5 Discussion.- 2.5 Summary.- 2.6 Semantics.- 2.7 Notes and Suggestions for Further Reading.- 3. A Presentation of Logical Tools.- 3.1 Some Applications of Logic.- 3.1.1 Programming.- 3.1.2 Sums and Unions.- 3.1.3 Chasing Paradoxes Away.- 3.2 Antecedents.- 3.3 The Different Branches of Logic.- 3.3.1 Model Theory.- 3.3.2 Proof Theory.- 3.3.3 Axiomatic Set Theory and Type Theory.- 3.3.4 Computability Theory.- 3.4 Mathematical Reminders.- 3.4.1 Set Notations.- 3.4.2 Logical Operators.- 3.4.3 Relations and Functions.- 3.4.4 Operations.- 3.4.5 Morphisms.- 3.4.6 Numbers.- 3.4.7 Sequences.- 3.5 Well-founded Relations and Ordinals.- 3.5.1 Loop Variant and Well-founded Relation.- 3.5.2 Examples.- 3.5.3 Well-founded Induction.- 3.5.4 Well Orders and Ordinals.- 3.6 Fixed Points.- 3.7 More About Computability.- 3.7.1 Primitive Recursion.- 3.7.2 Recursion, Decidability.- 3.7.3 Partial Recursion, Semi-Decidability.- 3.7.4 A Few Words on Logical Complexity.- 3.8 Notes and Suggestions for Further Reading.- 4. Hoare Logic.- 4.1 Introducing Assertions in Programs.- 4.2 Verification Using Hoare Logic.- 4.2.1 Rules of Hoare Logic.- 4.2.2 Bounded Linear Search Program.- 4.3 Program Calculus.- 4.3.1 Calculation of a Loop.- 4.3.2 Calculation of an Assignment Statement.- 4.3.3 Weakest Precondition.- 4.4 Scope of These Techniques.- 4.5 Notes and Suggestions for Further Reading.- 5. Classical Logic.- 5.1 Propositional Logic.- 5.1.1 Atomic Propositions.- 5.1.2 Syntax of Propositions.- 5.1.3 Interpretation.- 5.2 First-order Predicate Logic.- 5.2.1 Syntax.- 5.2.2 Example of the Table.- 5.2.3 Interpretation.- 5.3 Significant Examples.- 5.3.1 Equational Languages.- 5.3.2 Peano Arithmetic.- 5.4 On Total Functions, Many-sorted Logics.- 5.5 Second-order and Higher-order Logics.- 5.6 Model Theory.- 5.6.1 Definitions.- 5.6.2 Some Results of Model Theory; Limitations of First-Order Logic.- 5.7 Notes and Suggestions for Further Reading.- 6. Set-theoretic Specifications.- 6.1 The Z Notation.- 6.1.1 Schemas.- 6.1.2 Operations.- 6.1.3 Example.- 6.1.4 Relations and Functions.- 6.1.5 Typing.- 6.1.6 Refinements.- 6.1.7 Usage.- 6.2 VDM.- 6.2.1 Origins.- 6.2.2 Typing.- 6.2.3 Operations.- 6.2.4 Functions.- 6.2.5 Three-valued Logic.- 6.2.6 Usage.- 6.3 The B Method.- 6.3.1 Example.- 6.3.2 Abstract Machines.- 6.3.3 Simple Substitutions and Generalized Substitutions.- 6.3.4 The B Refinement Process.- 6.3.5 Modularity.- 6.4 Notes and Suggestions for Further Reading.- 7. Set Theory.- 7.1 Typical Features.- 7.1.1 An Untyped Theory.- 7.1.2 Functions in Set Theory.- 7.1.3 Set-theoretic Operations.- 7.2 Zermelo¡ªFraenkel Axiomatic System.- 7.2.1 Axioms.- 7.2.2 Reconstruction of Usual Set-theoretic Concepts.- 7.2.3 The Original System of Zermelo.- 7.3 Induction.- 7.3.1 Reconstruction of Arithmetic.- 7.3.2 Other Inductive Definitions.- 7.3.3 The Axiom of Separation.- 7.3.4 Separation of a Fixed Point.- 7.3.5 Ordinals.- 7.4 Sets, Abstract Data Types and P


Information Provided By: : Aladin

New Arrivals Books in Related Fields