8. Type Systems Flashcards
Type systems are most widely used form of static analysis. T/F
True
Motivation for type system (basic example of what it is/does)
required a boolean but you gave it a float.
Tried to return an array when the function expected to return an int.
What is a type?
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
More types
Foo is the set of all objects of class Foo List is set of all Lists of Integer objects
Abstraction
represents sets of concrete values as abstract values
In type systems, every concrete value is an element of some abstract value.
every concrete value has a type
english to inference rule for
if e1 has type int and e2 has type int, then e1+e2 has type int
(e1:int ^ e2:int)=> e1+e2 : int
Notation for inference rules
|-Conclusion
Inference rule axiom
|-e:t
something with no hypotheses but we know is true
Type judgement
Hypotheses and conclusions are type judgments that take the form:
|-e:t
|-
it is provable that
Schema
something very basic and template like.
|- i : int
i is integers
Rules for integers: inference rule for e1+e2
|-e1:int |-e2:int
————————- [Add] (name)
|-e1+e2 :int
Hypotheses state facts about ______
Conclusions state facts about ______
sub-expressions
entire expression
Bound variable
a variable in an expression that is defined within the expression
Free variable
in an expression not defined within the expression
Type Environments notation: What does this mean in english?
A |- e : t
Under the assumption that variables have types given by A, it is provable that the expression has type t
Explain what the following means and when it is used:
A[ x->t]
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.
A |- e1 e2 : t2
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
Type Derivation
Procedure to determine the type of a program if one exists.
come back to this 24/25
side condition
additional condition that needs to be satisfied for the inference rule to be valid.
looks like;
t1=t2
Soundness verifies _____
absence of a class of errors
Soundness comes at a price:
false positives
Unsound analysis =
reduced false positives
introduces false negatives
