# Introduction To Formalism

• 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
• Prerequisites

• Need to be able to program a computer
• High School algebra
• Ability to work hard

• Maybe a project

# Why Formalism?

• 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

# Why Z?

• 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

• 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

# Introducing Z

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

• Formatters
• 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