Lecture Notes

The notes are rather sparse and only include definitions and the like (and maybe some worked, tedious exercises). They are a good summary for later reference but are by no means a substitute for the actual lectures and/or textbook.

Notes (handout)	Notes (overhead presentation)	Relevant textbook material
Introduction	Introduction	some Chapter 7
Alphabets, strings, and languages	Alphabets,...	Chapter 7
State transition diagrams	State transition diagrams	Chapter 8 (except Section 8.5)
Regular languages	Regular languages	Chapter 91
Context-free languages	Context-free languages	Chapter 10
Parsing (example)	Parsing (example)	Chapter 11, bottom-up parsing extra2
Algorithm specification	Algorithm specification	Chapter 1
Algorithm verification + example + array example	Verification + example + array example	Chapters 2 and 4
Algorithm verification examples	Algorithm verification examples	Chapter 3
Introduction to formal methods	Introduction to formal methods	Section 8.5, extra3

Lecture recording

My lectures are recorded, as follows:

• Introduction: Lecture 1
• Alphabets, strings, and languages: Lecture 2, Lecture 3, Lecture 4
• State transition diagrams: Lecture 5, Lecture 6, first about 45 minutes of Lecture 7 (out of which the first about 10 minutes not recorded due to software failure)
• Regular expressions and state transition diagrams: last about 30 minutes of Lecture 7, Lecture 8, Lecture 10
• Context-free languages: Lecture 11 (not captured due to equipment failure), Lecture 12, first 30 minutes of Lecture 13
• Parsing: last 45 minutes of Lecture 13, first 45 minutes of Lecture 14
• Software specification: last about 25 minutes of Lecture 14, first hour (about 50 minutes of the recording) of Lecture 15 (first about 10 minutes of the lecture were not recorded)
• Deductive verification: last 15 minutes of Lecture 15, Lecture 16, Lecture 17, Lecture 18, Lecture 19, Lecture 20, a bit (about 10 minutes) at the beginning of Lecture 21
• Introduction to formal methods: Lecture 21, Lecture 22

Footnotes

... Chapter 9¹

Here is an example of practical application of regular languages: The file scanner.l describes a complete lexical analyzer (or scanner) for a Java-like programming language. This is the input of Flex which generates C code that implements one big finite automaton (which in turn implements the actual lexical analysis). You will notice that the regular expressions that define the lexical structure of a programming language are not overly complicated, but on the other hand there are lots of them; the resulting finite automaton (that is used for the actual lexical analysis) is therefore quite large.

... extra²

Here is an example of practical application of context-free languages: The file parser.y describes a complete parser for a Java-like language. This is the input of Yacc or its successor Bison which generate C/C++ code that implements the actual parsing.

... extra³

This introduction in formal methods is based on Schneider's text (see below) and to some degree on Section 8.5. Note however that reading Schneider (to say nothing about the rest of the references mentioned below!) is definitely overkill for this course. In any event, here are some additional readings for the reader interested in formal methods: Comprehensive presentations of CSP include The Theory and Practice of Concurrency by A. W. Roscoe and Concurrent and Real Time Systems: The CSP Approach by S. A. Schneider. A different approach to the same problem is model checking. A good introduction to this matter is Model Checking by E. M. Clarke, O. Grumberg and D. Peled (available in the Bishop's library). Yet another approach is model-based testing. An introduction to this subject is Model-Based Testing of Reactive Systems (also available in the library).