Proving Safety Properties using Types
We next discuss general techniques for proving absence of errors in programs
This also tells us how to prove that our type systems are meaningul (sound)
Safety Properties of Programs
Given a one-step reduction relation , as in Operational Semantics of Lambda with Letrec, a finite execution is a sequence of states
where is one of the possible initial states of the program.
A safety property of a program is a property of finite executions of this program
In addition to safety, there are other kinds of properties, in particular liveness
- require reasoning about infinite executions
- example: the program always reaches a given program point
- in this compilers course we talk only about safety
Important kind of safety properties: program does not crash with a run-time error
We represent run-time errors using a predicate error(s) which is true iff state s is a run-time error
- we want to prevent programs from reaching state s such that error(s)
A finite execution trace is error-free iff for all
- this definition shows that “program cannot reach a run-time error” is a safety property
Examples of Run-Time Errors
Depending on the programming language, run-time errors can include
- null dereference in Java
- array bounds error in Java
- failed type cast in Java
- division by zero in Java
- attempt to multiply integer with a string
- attempt to invoke a non-existing method on an object in Smalltalk
Example Error in Python Program
Example program in the Python (programming language)
i = 40000000 while i > 0: i = i - 1 width = 30 height = 20 important = "learning" area = width * height fishy = important / height
Call this program 'test.py'
If you run it, you will first have to wait for a bit, and then you will get a result like this:
Proving Safety by Induction
Usually we use mathematical induction to prove safety (including absence of run-time errors)
- show a property for all traces of length zero
- show that if property holds for all traces of length , it holds for traces of length
Problem: if , it does not mean
- example: no error by step , but then program calls a method that will cause a run-time error in step
- see above examples
As in many other examples, we typically need to strengthen the induction hypothesis
Example: straight-line program that uses int and boolean types
x = 1; y = bool; z = 70; --> z = z / x; x = x - 1; z = z / x;
Just because there was no error so far, it does not mean that later there will not be e.g. 'x = z / x' when x=0
x = 1; y = bool; z = 70; --> z = z / x; x = x + 1; z = z / x;
We need a stronger induction hypothesis. For example, perhaps we can prove that all values of variables used after '/' are positive
We call a stronger induction hypothesis inductive invariant and denote it . It is property for which inductive proof works:
- for each initial state , we have
- if and , then
To prove absence of errors, we find an inductive invariant that ensures absence of errors: for all configurations , implies .
All states in execution sequence satisfy , so they satisfy
Ensuring Safety Using Types
One of the goals of static type systems is to ensure absence of crashes due to certain run-time type errors
We say that type system is sound if for program implies that execution of causes no run-time type errors of certain kind
- example of errors prevented: adding int and bool values, calling non-existing method in Java
- some errors may remain: division by zero, null dereference
Because absence of errors is a safety property, we can prove it using an inductive invariant
Soundness theorem for a type system shows that if program type checks, then there is a property or program configurations such that
- is an inductive invariant
- implies that there are no run-time errors
If program configuration is a program itself, then usually says that type checks
- if there is state, then it must talk about type checking in a given program state
- we can typically represent states as certain 'map' expressions
Summary of Type Soundness Proofs
To prove type soundness, we need to do the following:
- define program configurations and operational semantics
- show how to define property for a given program that type checks
- show that every such is an inductive invariant
- show that if holds, then certain run-time errors will not happen