|
|
|
|
@ -46,7 +46,7 @@ date: November 21, 2018
|
|
|
|
|
- Model "essence" of real languages |
|
|
|
|
|
|
|
|
|
## 2. Formalize what programs "do" |
|
|
|
|
- Usually: run it on a machine and find out! |
|
|
|
|
- Run it on a machine and find out? |
|
|
|
|
- Not very useful for proofs... |
|
|
|
|
- Formalize behavior mathematically, on paper |
|
|
|
|
- Discard "unimportant" details |
|
|
|
|
@ -115,7 +115,7 @@ date: November 21, 2018
|
|
|
|
|
|
|
|
|
|
# Operational Semantics |
|
|
|
|
|
|
|
|
|
## Programs execute by "stepping" |
|
|
|
|
## Execute by "stepping" |
|
|
|
|
- Start with program |
|
|
|
|
- Imperative: plus variable setting |
|
|
|
|
- In each step, perform update: |
|
|
|
|
@ -137,8 +137,8 @@ date: November 21, 2018
|
|
|
|
|
- A type $\tau$ describes a class of programs |
|
|
|
|
- Usually: well-behaved in some way |
|
|
|
|
- Can automatically check if program has type $\tau$ |
|
|
|
|
- Type of program depends on types of its pieces |
|
|
|
|
- Scales to large programs |
|
|
|
|
- Type of program depends on types of components |
|
|
|
|
- Analysis scales to large programs |
|
|
|
|
|
|
|
|
|
## Example |
|
|
|
|
|
|
|
|
|
@ -146,18 +146,18 @@ date: November 21, 2018
|
|
|
|
|
- Lightweight |
|
|
|
|
- Checking types is simple, automatic |
|
|
|
|
- Don't need to run program |
|
|
|
|
- Intuitive meaning |
|
|
|
|
- Natural and intuitive |
|
|
|
|
- Can't add a String to a Boolean |
|
|
|
|
- Programmers often think in terms of types |
|
|
|
|
- Identify correct programs |
|
|
|
|
|
|
|
|
|
## Weaknesses |
|
|
|
|
- Programmer may need to add some type hints |
|
|
|
|
- Extra annotations in program |
|
|
|
|
- Programmer may need to add annotations |
|
|
|
|
- Extra hints for compiler |
|
|
|
|
- Common for more complex types |
|
|
|
|
- Compiler sometimes rejects correct programs |
|
|
|
|
- Figuring out why can be very frustrating |
|
|
|
|
- May need to write program in more awkward form |
|
|
|
|
- May need to write program in less natural form |
|
|
|
|
|
|
|
|
|
## Types can be complex |
|
|
|
|
- Simpler types |
|
|
|
|
@ -170,9 +170,9 @@ date: November 21, 2018
|
|
|
|
|
- ... |
|
|
|
|
|
|
|
|
|
## Prove: soundness |
|
|
|
|
- "Soundness theorem" |
|
|
|
|
- Relate type system to operational behavior |
|
|
|
|
- If program has a type, it should be well-behaved |
|
|
|
|
- Relate type system to operational behavior |
|
|
|
|
- "Soundness theorem" |
|
|
|
|
- Many possible notions of "well-behaved" |
|
|
|
|
- Don't add Strings to Bools |
|
|
|
|
- Don't mix public and private data |
|
|
|
|
|
