Introduction To Formalism
Copyright (c) 2016 Bart Massey
About This Course
First part of a two-part sequence
Teaches the concepts of CS 250 / 251
In the setting of formal specification of programs
- Inherently more work
- Hopefully clearer, easier and more motivating
- Need to be able to program a computer
- High School algebra
Ability to work hard
- Reading, homework, quizzes, exams
- Maybe a project
This is our math
- Calculus is useful
- Most of what we do needs / can use discrete math
Substitute for computation
- Provides more understanding
- Is feasible in places where computation isn't
- Can provide stronger guarantees (proof vs testing, inspection)
Modeling and analysis
Program ~~~~~~~~> Behavior | ^ | | | | v | Modeling -------> Analysis
- Modeling: describe a situation, problem or solution formally
- Analysis: figure out what the model means / implies
Discrete math notation is nonstandardized
- Things like whether zero is a "natural number"
- Few tools available to process it
Discrete math notation is not tuned to computing
- Notions of state and state transformation are absent
There's this really good book
Applicable => Motivated
- It's hard to care about this stuff unless you're doing things with it
- Makes it easier to remember
- Suggests a particular order of topics
We are terrible at getting programs right
- Huge impacts in mission-critical / safety-critical software
- Even on ordinary projects, lots of extra cost due to rework
Here's a very simple Z specification using ASCII notation.
| square : N -> N |---------------- | forall a : N @ square(a) = a * a | isqrt : N -> N |--------------- | forall a : N @ | square(isqrt(a)) <= a < square(isqrt(a) + 1)
Things to note:
- Specification describes typed functions
- Specification is declarative: describes what it is rather than how to compute it.
- Specification is perfectly precise.
The Therac 25 Disaster
Motivating example for the textbook
Produced in 1982: killed or seriously injured six people between 1985 and 1987
"The defect was as follows: a one-byte counter in a testing routine frequently overflowed; if an operator provided manual input to the machine at the precise moment that this counter overflowed, the interlock would fail."
The software was a huge mess, and no real specification existed.
You think that was then and this is now...
Formal Specification Is "Easy"
- Lots of work per line of specification
- But this work is mostly figuring out that needs to be done anyway
- The notation isn't too hard to learn (on faith for now)
Tools, Proofs and Whatnot
There are a number of ancient tools available for dealing with Z
- Typecheckers, which also check syntax
- Proof tools and assistants
We will mostly stick with simple tools
The standard notation for Z is LaTeX
- Maybe you should learn it anyhow
- We will try not to require it
Most of the value is in the modeling
- We prove properties, not "correctness"
- Usually simple properties like soundness and completeness
- Proofs are not usually necessary
The Rest Of The Course
Dive into Z
Write formal models
Analyze and prove model properties