|
|
| | |
|
|
|
Requirement: Safety from errors during the execution of the program
is a major concern in PL design.
Solution: Safety can be achieved by two PL features (by one of them or a combination of both):
runtime checks
static checks by a static type system component of the language
| |
|
|
|
specifies
|
|
| | Safe expression (program fragment)
|
«A program fragment is safe
if it does not cause untrapped errors to occur »
[TS]
|
|
| | Well behaved
| |
«A progam fragment
is said to have good behavior, or equivalently to be well behaved,
if it does not cause any forbidden error to occur.
...
In particular, a well behaved fragment is safe »
[TS]
|
|
«Untyped languages
may enforce safety by performing run time checks »
[TS]
| untrapped errors = runtime errors => safe |
|
makes occur 
| event
| EXECUTION ERROR
|
«The most obvious symptom of an execution error
is the occurence of an unexpected software fault,
such as an illegal instruction fault or an illegal memory reference fault.
There are, however, more subtle kinds of execution errors
that result in data corruption without any immediate symptoms »
[TS]
| |
| |
| |
|
|
| Untrapped
| | [Hardware] trapped
|
| go unnoticed (for a while) and later cause arbitrary behavior
| | stop the computation immediately (= software fault ?)
| |
| |
| |
| |
|
| runtime [type] error
| | value mis- interpretation
| | forbidden
& trapped
| | allowed
|
| raised when runtime check fails
("software trapped")
| | the prototypical case of a type error
| | Eg. illegal memory access
| Eg. divide by zero, dereferencing nil
| | |
|
| | prog. lang.
| Safe language
| |
«Languages
where all program fragments are safe are called safe languages.
Therefore, safe languages rule out the most insidious form of execution errors:
the ones that may go unnoticed »
[TS]
|
| |
|
|
«[Statically] Typed languages
may enforce safety by statically rejecting all programs that are potentially unsafe.
Typed languages may also use a mixture of
run time and static checks »
[TS]
|
|
| Strongly checked
|
«A language
where all of the (legal) programs have good behavior
is called strongly checked »
[TS]
|
|
|
|
| legal programs < well-behaved programs => safe |
|
| |
|
RT checking
«In a dynamically typed language most operations are type-checked
just before they are performed »
[TyOOL]
|
| |
|
«In a traditional value-oriented language, one of the major
rôles of the type system is to prevent the misinterpretation of
values » [Emerald, 1f].
| |
|
«Typed languages usually aim to rule out also large classes of trapped errors,
along with the untrapped ones »
[TS]
|
\|/
| |
|
«[T]here are software faults,
such as divide by zero and dereferencing nil,
that are not normally prevented by type systems »
[TS]
|
| | |
| Forbidden Errors
|
«For any given language, we may designate a subset of the possible execution errors
as forbidden errors. The forbidden errors should include all of the untrapped
errors, plus a subset of the trapped errors »
[TS]
|
|
|
|
|
|
\|/
|
| | |
|
