8. Type Systems

Question 1

Type systems are most widely used form of static analysis. T/F

Answer 1

True

Question 2

Motivation for type system (basic example of what it is/does)

Answer 2

required a boolean but you gave it a float.

Tried to return an array when the function expected to return an int.

Question 3

What is a type?

Answer 3

A type is a set of values
int is a set of all integers between -2^31 and the opposite of that

Example of an abstract value. Represents a set of concrete values

Question 4

More types

Answer 4

Foo is the set of all objects of class Foo
List is set of all Lists of Integer objects

Question 5

Abstraction

Answer 5

represents sets of concrete values as abstract values

Question 6

In type systems, every concrete value is an element of some abstract value.

Answer 6

every concrete value has a type

Question 7

english to inference rule for

if e1 has type int and e2 has type int, then e1+e2 has type int

Answer 7

(e1:int ^ e2:int)=> e1+e2 : int

Question 8

Notation for inference rules

Answer 8

|-Conclusion

Question 9

Inference rule axiom

Answer 9

|-e:t

something with no hypotheses but we know is true

Question 10

Type judgement

Answer 10

Hypotheses and conclusions are type judgments that take the form:
|-e:t

Question 11

|-

Answer 11

it is provable that

Question 12

Schema

Answer 12

something very basic and template like.

|- i : int
i is integers

Question 13

Rules for integers: inference rule for e1+e2

Answer 13

|-e1:int |-e2:int
————————- [Add] (name)
|-e1+e2 :int

Question 14

Hypotheses state facts about ______

Conclusions state facts about ______

Answer 14

sub-expressions

entire expression

Question 15

Bound variable

Answer 15

a variable in an expression that is defined within the expression

Question 16

Free variable

Answer 16

in an expression not defined within the expression

Question 17

Type Environments notation: What does this mean in english?

A |- e : t

Answer 17

Under the assumption that variables have types given by A, it is provable that the expression has type t

Question 18

Explain what the following means and when it is used:

A[ x->t]

Answer 18

means “A modified to map x to type t”
used when x would be a free variable in a conclusion. Include the statement after the environment A in the hypothesis. Lesson 22.

Question 19

A |- e1 e2 : t2

Answer 19

if under the environment A, it is provable that e1 has type t1->t2,
and under the environment A it is provable that e2 has type t2,
then
it is provable that calling e1 with argument e2 will yield type t2

Question 20

Type Derivation

Answer 20

Procedure to determine the type of a program if one exists.

come back to this 24/25

Question 21

side condition

Answer 21

additional condition that needs to be satisfied for the inference rule to be valid.
looks like;
t1=t2

Question 22

Soundness verifies _____

Answer 22

absence of a class of errors

Question 23

Soundness comes at a price:

Answer 23

false positives

Question 24

Unsound analysis =

Answer 24

reduced false positives

introduces false negatives

Question 25

Global analysis

Answer 25

requires overall environment
Usually technically simpler than local analysis
may need extra work to model environments for unfinished programs

Question 26

local analysis

Answer 26

more flexible in application

technically harder: need to allow unknown parameters, more side conditions

Question 27

flow insensitive

Answer 27

we don’t give afuck about the order (flow) of statementsq

Question 28

flow sensitive analysis downside

Answer 28

expensive/complex

polynomial increase in cost over flow insensitive due to each statement having its own model of state