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

• 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 

The Rest Of The Course

• Dive into Z

• Write formal models

• Analyze and prove model properties