Formal Methods in Computer Science

Jiacun Wang

• Publisher: Chapman and Hall/CRC
• Year: 2019
• Print ISBN: 9780367225704
• eBook ISBN: 9781498775359
• Topic: Computer Science
• Subtopic: Computer Engineering
• Index: Computer Science

This textbook gives students a comprehensive introduction to formal methods and their application in software and hardware specification and verification. It has three parts: The first part introduces some fundamentals in formal methods, including set theory, functions, finite state machines, and regular expressions. The second part focuses on logi

1

Set Theory and Functions

The concepts of a set and that of a function are well known to most people in an informal manner. After all, it doesn’t take a mathematical genius to talk about a tea set as having four cups, four saucers, a tea pot, a sugar bowl, and a creamer. Anyone who has studied basic algebra in high school knows that the square function applied to a number x produces a number y such that x times x = y. These are nice informal everyday understandings for sets and functions. However, this informal understanding is not sufficient to generate unambiguous and detailed specifications for use in describing a program.

To be useful in specifying programs and systems, a deeper and more formal understanding of these two concepts is necessary. It requires the clarity, specificity, and precision of mathematics to unambiguously specify the procedures, operations, and functions of a computer program.

In this chapter, set theory and functions are introduced and defined. The introduction uses simple language to define the key concepts in a naïve formalism, rather than a strictly logical formal definition. The formal definition of sets and functions requires symbolic logic, which is introduced in a later chapter. Sets and functions will be revisited using a logic-based formalism. This chapter addresses two basic questions:

1. What is a set?

2. What is a function?

Examples of where sets and functions can be used in specifying program behavior will be given.

1.1 Basic Set Definitions

The exploration of set theory begins by establishing a simple vocabulary that allows for discussion of the concepts without an excessive burden of mathematics. It slowly develops the mathematics of sets as the chapter progresses.

A set is an abstract collection of distinct objects. A set, denoted by {}, exists as an abstraction for some collection of objects where the collection is treated as a whole. It is an object in its own right, albeit an abstract object. For example, a flock of birds (i.e., a set of birds) treats the entire collection of birds as a single entity although it is made up of individual birds.

An object that is part of a collection is an element or member of the set. The terms element and member are used interchangeably. This book gives preference to the term member. A member of a set is shown within the curly braces. The set containing the three colors RED, GREEN, YELLOW is {RED, GREEN, YELLOW}. The curly braces indicate the set and the values between the curly braces are the members of that set. The member can be an abstraction (e.g., a word, number, or even another set) or a concrete thing (e.g., car, plane, or teacup).

Membership in a set is an all-or-nothing kind of deal. A thing is either a member of the set or it isn’t. It can’t be a partial member or be a member m...

Table of contents

• Cover
• Half Title
• Title Page
• Copyright Page
• Table of Contents
• Preface
• Acknowledgments
• Authors
• 1. Set Theory and Functions
• 2. Finite State Machine
• 3. Regular Expressions and Languages
• 4. Propositional Logic
• 5. Predicate Logic
• 6. Temporal Logic
• 7. Formal Verification by Model Checking
• 8. Petri Nets
• 9. Timed Petri Nets
• 10. Colored Petri Nets
• Index