程序代写代做代考 c++ Java Haskell javascript go Lambda Calculus C Safety and Liveness Type Safety Exceptions

Safety and Liveness Type Safety Exceptions
Safety and Liveness; Exceptions
Christine Rizkallah
CSE, UNSW Term 3; 2020
1

Safety and Liveness Type Safety Exceptions
Program Properties
Consider a sequence of states, representing the evaluation of a program in a small step semantics (a trace):
σ1 􏰀→σ2 􏰀→σ3 􏰀→···􏰀→σn
Observe that some traces are finite, whereas others are infinite. To simplify things, we’ll make all traces infinite by repeating the final state of any terminating state infinitely. Such infinite sequences of states are called behaviours.
A correctness property of a program is defined to be a set of behaviours.
2

Safety and Liveness Type Safety Exceptions
Safety vs Liveness
1 A safety property states that something bad does not happen. For example: I will never run out of money.
These are properties that may be violated by a finite prefix of a behaviour.
2 A liveness property states that something good will happen. For example:
If I start drinking now, eventually I will be smashed.
These are properties that cannot be violated by a finite prefix of a behaviour.
4

Safety and Liveness Type Safety Exceptions
Combining Properties Safety properties we’ve seen before
5

Safety and Liveness Type Safety Exceptions
Combining Properties
Safety properties we’ve seen before
Partial correctness (Hoare Logic) Static semantics properties
Liveness properties we’ve seen before
Termination Confluence
Theorem
Every property is the intersection of a safety and a liveness property. The proof of this involves topology (specifically metric spaces).
8

Safety and Liveness Type Safety Exceptions
Types
What sort of properties do types give us?
9

Safety and Liveness Type Safety Exceptions
Types
What sort of properties do types give us?
Adding types to λ-calculus eliminates terms with no normal forms.
(x : τ) ∈ Γ x : τ1,Γ ⊢ e : τ2 Γ ⊢ e1 : τ1 → τ2 Γ ⊢ e2 : τ1 Γ ⊢ x : τ λx. e : τ1 → τ2 Γ ⊢ e1 e2 : τ2
Remember (λx. x x) (λx. x x)? Trying to type this requires an infinite type τ1 =τ1 →τ2.
Theorems
Each well typed λ-term always reduces to a normal form (strong normalisation). Furthermore, the normal form has the same type as the original term (subject reduction).
This means that all typed λ-terms terminate!
12

Safety and Liveness Type Safety Exceptions
With Recursion
MinHS, unlike lambda calculus, has built in recursion. We can define terms like: (recfunf ::(Int→Int)x=f x)3
Which has no normal form or final state, despite being typed. What now?
13

Safety and Liveness Type Safety Exceptions
Type Safety
Type safety is the property that states:
Well-typed programs do not go wrong.
By “go wrong”, we mean reaching a stuck state — that is, a non-final state with no outgoing transitions. What are some examples of stuck states?
There are many other definitions of things called “type safety” on the internet, but they are all incorrect.
15

Safety and Liveness Type Safety Exceptions
Progress and Preservation
We want to prove that a well-typed program either goes on forever or reaches a final state. We prove this with two lemmas.
How to prove type safety
1 Progress, which states that well-typed states are not stuck states. That is, if an expression e : τ then either e is a final state or there exists a state e′ such that e 􏰀→ e′.
2 Preservation, which states that evaluating one step preserves types. That is, if anexpressione:τ ande􏰀→e′,thene′ :τ.
16

Safety and Liveness Type Safety Exceptions
In the real world
Which of the following languages are type safe? C
C++ Haskell Java Python Rust MinHS
MinHS
23

Safety and Liveness Type Safety Exceptions
In the real world
Which of the following languages are type safe? C No
C++ No
Haskell Yes
Java Yes
Python Yes
Rust Yes (except for unsafe) MinHS Not type safe yet!
Why is MinHS not type safe?
24

Safety and Liveness Type Safety Exceptions
Division by Zero
We can assign a type to a division by zero:
(Num 3) : Int (Num 0) : Int (Div (Num 3) (Num 0)) : Int
But there is no outgoing transition from this state (nor is it final)! ⇒ We have violated progress.
We have two options:
1 Change the static semantics to exclude division by zero. This reduces to the halting problem, so we would be forced to overapproximate.
2 Change the dynamic semantics so that the above state has an outgoing transition.
27

Safety and Liveness Type Safety Exceptions
Our Cop-Out
Add a new state, Error, that is the successor state for any partial function: (Div v (Num 0)) 􏰀→M Error
28

Safety and Liveness Type Safety Exceptions
Our Cop-Out
Add a new state, Error, that is the successor state for any partial function: (Div v (Num 0)) 􏰀→M Error
Any state containing Error evaluates to Error:
(Plus e Error) 􏰀→M Error (Plus Error e) 􏰀→M Error
(If Error t e) 􏰀→M Error
(and so on – this is much easier in the C machine!)
29

Safety and Liveness Type Safety Exceptions
Type Safety for Error
We’ve satisfied progress by making a successor state for partial functions, but how should we satisfy preservation?
Error :
30

Safety and Liveness Type Safety Exceptions
Type Safety for Error
We’ve satisfied progress by making a successor state for partial functions, but how should we satisfy preservation?
Error : τ
31

Safety and Liveness Type Safety Exceptions
Type Safety for Error
We’ve satisfied progress by making a successor state for partial functions, but how should we satisfy preservation?
Error : τ That’s right, we give Error any type.
32

Safety and Liveness Type Safety Exceptions
Dynamic Types
Some languages (e.g. Python, JavaScript) are called dynamically typed. This is more accurately called unityped as they achieve type safety with the trivial type system containing only one type, here written ⋆, and only one typing rule1:
Γ⊢e:⋆
They achieve type safety by defining execution for every syntactically valid expression, even those that are not well typed.
Some languages make sensible decisions like evaluating to an error state, whereas other languages make alternative decisions like trying to perform operations on diverse kinds of data.
1The things these languages call types are part of values. They aren’t types.
34

Safety and Liveness Type Safety Exceptions
Exceptions
Error may satisfy type safety but it’s not satisfying as a programming language feature — when an error occurs, we may not want to crash the program. We will add more fine grained error control – exceptions – to MinHS.
Example (Exceptions)
try/catch/throw in Java, setjmp/longjmp in C, try/except/raise in Python. Exceptions Syntax
Raising an Exception Concrete raise e
Abstract (Raise e)
Handling an Exception
try e1 handle x ⇒ e2 (Try e1 (x. e2))
35

Safety and Liveness
Type Safety
Exceptions
Example
Informal Semantics
try
if y ≤ 0 then
raise DivisorError else
(x/y) handle err ⇒ −1
For an expression (try e1 handle x ⇒ e2) we
1 Evaluate e1
2 If raise v is encountered while evaluating e1, we bind v to x and evaluate e2.
Note that it is possible for try expressions to be nested. The inner-most handle will catch exceptions. Handlers may re-raise exceptions.
36

Safety and Liveness Type Safety Exceptions
Static Semantics
The type given to exception values is usually some specific blessed type τE that is specifically intended for that purpose. For example, the Throwable type in Java. In dynamically typed languages, the type is just the same as everything else (i.e. ⋆).
Typing Rules
Γ⊢e:τE Γ⊢e1:τ x:τE,Γ⊢e2:τ Γ ⊢ (Raise e) : τ Γ ⊢ (Try e1(x. e2)) : τ
37

Safety and Liveness Type Safety Exceptions
Dynamic Semantics
Easier to describe using the C Machine. We introduce a new type of state, s ≺≺ v, that means an exception value v has been raised. The exception is bubbled up the stack s until a handler is found.
Evaluating a Try Expression
s ≻ (Try e1 (x. e2))
Returning from a Try without raising (Try􏰈(x.e2))◃s ≺ v
Evaluating a Raise expression s≻ (Raise e )
Raising an exception
(Raise 􏰈) ◃ s ≺ v Catching an exception
(Try 􏰈 (x. e2)) ◃ s ≺≺ v
Propagating an exception
f ◃ s ≺≺ v
􏰀→C (Try􏰈(x.e2))◃s ≻ e1
􏰀→C s≺v
􏰀→C (Raise 􏰈)◃s ≻ e
􏰀→C s ≺≺ v
􏰀→C s ≻ e2[x:=v] 􏰀 →C s ≺≺ v
38

Safety and Liveness Type Safety Exceptions
Efficiency Problems
The approach described above is highly inefficient. Throwing an exception takes linear time with respect to the depth of stack frames!
Only the most simplistic implementations work this way. A much more efficient approach is to keep a separate stack of handler frames.
Handler frames
A handler frame contains:
1 A copy of the control stack above the Try expression.
2 The exception handler that is given in the Try expression.
We write a handler frame that contains a control stack s and a handler (x. e2) as (Handle s (x. e2)).
39

Safety and Liveness Type Safety Exceptions
Efficient Exceptions
Evaluating a Try now pushes the handler onto the handler stack and a marker onto the control stack.
(h,s)≻(Trye1 (x.e2))􏰀→C (Handles (x.e2) ◃h,(Try􏰈)◃s)≻e1 Returning without raising in a Try block removes the handler again:
(Handles(x.e2) ◃h,(Try􏰈)◃s)≺v􏰀→C (h,s)≺v
Raising an exception now uses the handler stack to immediately jump to the handler:
(Handles(x.e2) ◃h,(Raise􏰈)◃s′)≺v􏰀→C (h,s)≻e2[x:=v]
40

Safety and Liveness Type Safety Exceptions
Exceptions in Practice
While exceptions are undoubtedly useful, they are a form of non-local control flow and therefore must be used carefully.
In Haskell, exceptions tend to be avoided as they make a liar out of the type system:
head :: [a] → a
In Java, checked exceptions may be used to allow the possibility of exception throws to
be tracked in the type system.
Monads
One of the most common uses of the Haskell monad construct is for a kind of error handling that is honest about what can happen in the types.
41

Related Posts