## Lecture 1-1

# Introduction To Formalism

Copyright (c) 2016 Bart Massey

# About This Course

**First part of a two-part sequence**Teaches the

*concepts*of CS 250 / 251In 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

- Reading, homework, quizzes, exams
- 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

- 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

# 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

- We prove

# The Rest Of The Course

Dive into Z

Write formal models

Analyze and prove model properties