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 $\leadsto$ , as in Operational Semantics of Lambda with Letrec, a finite execution is a sequence of states

$\begin{equation*} s_1 \leadsto s_2 \leadsto \ldots \leadsto s_n \end{equation*}$

where $s_1$ 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 $s_1 \leadsto \ldots \leadsto s_n$ is error-free iff $\lnot error(s_i)$ for all $1 \le i \le n$

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:

$ python test.py 
Traceback (most recent call last):
  File "test.py", line 9, in <module>
    fishy = important / height
TypeError: unsupported operand type(s) for /: 'str' and 'int'

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 $n$ , it holds for traces of length $n+1$

Problem: if $\lnot error(s_n)$ , it does not mean $\lnot error(s_{n+1})$

example: no error by step $n$ , but then program calls a method that will cause a run-time error in step $n+k$
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 $I$ . It is property for which inductive proof works:

for each initial state $s_1$ , we have $I(s_1)$
if $s_1 \leadsto \ldots \leadsto s_n$ and $I(s_1),\ldots,I(s_n)$ , then $I(s_{n+1})$

To prove absence of errors, we find an inductive invariant $I$ that ensures absence of errors: for all configurations $s$ , $I(s)$ implies $\lnot error(s)$ .

All states $s$ in execution sequence satisfy $I(s)$ , so they satisfy $\lnot error(s)$

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 $\Gamma_0 \vdash p:t$ for program $p$ implies that execution of $p$ 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 $I$ or program configurations such that

$I$ is an inductive invariant
$I$ implies that there are no run-time errors

If program configuration $s$ is a program itself, then $I(s)$ usually says that $s$ 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 $\leadsto$
show how to define property $I$ for a given program that type checks
show that every such $I$ is an inductive invariant
show that if $I$ holds, then certain run-time errors will not happen