Lecture Notes

The notes will be very sparse; I will only put in them definitions and the like (and maybe some worked, tedious exercises). The main matter will be discussed on the blackboard; these notes are just a mean to save me (and you too) some writing (and so some time).

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 + array example Verification + 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
Introduction to the computability theory Introduction to computability Chapter 12

Lecture recording

My lectures are recorded, as follows:

Except for Lecture 1 there are two videos for each lecture, one featuring the camera feed and the other featuring a capture of the front desk screen. The audio track is the same for both videos. You should probably start with the camera stream combined with a separate view of the respective PDF lecture notes, though for some lectures the screen capture might be more appropriate. You may even want to run both streams simultaneously (one of them muted).


... Chapter 91
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.
... extra2
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 code that implements the actual parsing.
... extra3
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).