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 / 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

Last modified: Tuesday, 5 January 2016, 11:51 AM