Safety as a Software Metric
Matthias Felleisen and Robert Corky Cartwright
Rice University
Why Safety as a Metric?
• Measuring Software: Syntax versus Semantics
• What is Programming Language Safety ?
• What Makes an Individual Program Safe ?
• How about Teaching Program Safety?
Why Measure Software?
• correct and efficient software
• maintainable software
• extensible software
What do Metrics Measure?
• lines of code
• number of procedures, gotos, loops, modules,
statements versus expressions, …
• in short: Syntactic Attributes of software
What should Metrics Measure?
• correctness
• extensibility
• maintainability
• in short: semantic and organizational attributes
Measuring Correctness is Difficult
• …
• goal: measure certain aspects of correctness
• specifically: assume the programming language is
safe, what kind of problems can we predict?
Safe Programming Languages
Safety -- A High-Level View (1)
“Close the valve by
10 degrees!”
“Turned the valve by
10 degrees!”
Safety -- A High-Level View (2)
“Close the valve by
10 degrees!”
“Turned the valve by
15 degrees!”
Safety -- A High-Level View (3)
“Close the valve by
10 degrees!”
Safety -- A High-Level View (4)
Safety -- A High-Level View (5)
C and C++ are NOT Safe!
int f(int n, int m) {
int r = n % m;
if (0 == r)
return m;
return f(m,r);
main() {
char a = 'a';
char b = 'b';
int mn[2] = {24,6};
char c = 'c';
char d = 'd';
Safety in Programming Languages
• a safe language protects every computational
primitive, e.g., +, *, if, vector-lookup, record
dereference, …
• protection is implemented with a mixture of compiletime and run-time checks
• safety guarantees errors are caught
• safety greatly increases effectiveness of debugging
• … is NOT just TYPE checking!
UNSAFE Languages
SAFE Languages
• Fortran
• ML
• C
• Eiffel
• C++
• Java
• Perl
• Scheme (untyped, but safe)
Safe Programs and Measuring Safety
Measuring the Safety of Programs
• programs in safe languages signal errors
• programs should not signal errors
• determine whether any computational primitive might
signal an error
• make programmers explain potential faults
MrSpidey: Measuring the Safety of Scheme Programs
• Scheme is a dialect of Algol and LISP
• lexical scope, first-class functions (“mini-objects”)
• LISP’s syntax (parentheses) and primitives (cons, car,
and cdr)
some function call, somewhere in the program
SYMBOLS are bad for +
general input shapes
Measuring Safety is More than Checking Types
• check general “data shapes”
• lists with at least N items
• vector references
• …
list with at least one NUMBER
NIL is not okay
An Elaborate Example from the Scheme Front-end
(let (<var> <rhs:exp>)
((lambda (<var>) <body:exp>)
… yields many checks
weak invariant
stronger invariant yields
stronger results
Teaching with Safety Metrics
Program Construction: Rice University, Fall 1998
• course on program safety
• understanding
• measuring
• based on Scheme and Java
On Safety of Languages and Programs
• programming language safety
• program safety
• theory and tools for “measuring” program safety
– logics that conservatively approximate semantics
– logics that extend the logic of type checking
The Pragmatics of MrSpidey
• using MrSpidey:
– checking
– understanding potential fault sites:
• data set
• data flow
– is it a problem with the program?
– is it a problem with the theory/tool?
– if the latter, can a re-organization help?
Hands-on Work
• homework assignments
– sets of problems for each bullet
– increasing complexity
– theory and practice
• project: implement sequential subset of Java
– modules and data invariants that cross boundaries
– exploring large pieces of code
Evaluation (1)
• course evaluation: excellent
• targeted questions:
– understanding of language safety
– understanding of program safety
– understanding of measuring safety with theorem
– effectiveness of homeworks versus project
Evaluation (2)
• Positives:
– appreciate safety
– appreciate tools
– appreciate theory
– understand the above
based on homework
• Negatives
– project too large
• new, semantics-based thinking about “metrics”
• extensions: measuring stronger invariants (numeric
constraints, polyvariant); measuring organization
• teaching: a good approach to have students
understand partial correctness
Thank You
Mike Fagan (92)
Andrew Wright (94)
Cormac Flanagan (96)
Matthew Flatt
Shriram Krishnamurthi
Robby Findler

Why Functional Programming Matters --