Types and Program Analysis

(1)

CS618: Program Analysis 2016-17 I

^st

Semester

Types and Program Analysis

Amey Karkare

karkare@cse.iitk.ac.in karkare@cse.iitb.ac.in

Department of CSE, IIT Kanpur/Bombay

karkare, CSE, IITK/B CS618 1/24

(2)

Reference Book

Types and Programming Languages by Benjamin C. Pierce

(3)

Type: Definition

(4)

Types in Programming

A collection ofvalues

+

(5)

Types in Programming

A collection ofvalues

The operations that are permitted on these values

+

(6)

Type System

A collection of rules for checking the correctness of usages of types

(7)

Type System

A collection of rules for checking the correctness of usages of types

“Consistency” of programs

(8)

The World of Programming Languages

Typed

(9)

Typed

C, C++, Java, Python, . . .

(10)

Typed

C, C++, Java, Python, . . . Untyped

(11)

Typed

C, C++, Java, Python, . . . Untyped

Assembly,any other?

(12)

Statically Typed Dynamically Typed Strongly Typed

Weekly Typed

(13)

Statically Typed Dynamically Typed Strongly Typed ML, Haskell, Pascal

(almost), Java (almost)

Weekly Typed

(14)

Lisp, Scheme

Weekly Typed

(15)

Lisp, Scheme

Weekly Typed C, C++

(16)

Lisp, Scheme

Weekly Typed C, C++ Perl

(17)

Applications of Type-based Analyses

Error Detection

(18)

Error Detection Language Safety

(19)

Error Detection Language Safety Verification

(20)

Error Detection Language Safety Verification Abstraction

(21)

Error Detection Language Safety Verification Abstraction Documentation

(22)

Error Detection Language Safety Verification Abstraction Documentation Maintenance

(23)

Error Detection Language Safety Verification Abstraction Documentation Maintenance Efficiency

(24)

Untyped Arithmetic Expression Language

t

_:= _{– terms}

(25)

t

_:= _{– terms}

true – constant true

(26)

t

_:= _{– terms}

false – constant false

(27)

t

_:= _{– terms}

false – constant false if

t

_then

t

_else

t

– conditional

(28)

t

_:= _{– terms}

t

_then

t

_else

t

– conditional

0 – constant zero

(29)

t

_:= _{– terms}

t

_then

t

_else

t

– conditional

succ

t

– successor

(30)

t

_:= _{– terms}

t

_then

t

_else

t

– conditional

succ

t

– successor

pred

t

– predecessor

(31)

t

_:= _{– terms}

t

_then

t

_else

t

– conditional

succ

t

– successor

pred

t

– predecessor

iszero

t

– zero test

(32)

Syntax: Inductive Definition

The set oftermsis the smallest setT such that

(33)

The set oftermsis the smallest setT such that 1. {true,false,0} ⊆ T

(34)

2. ift₁∈ T, then{succt₁,predt₁,iszerot₁} ⊆ T

(35)

2. ift₁∈ T, then{succt₁,predt₁,iszerot₁} ⊆ T

3. ift₁∈ T,t₂∈ T, andt₃∈ T thenift₁thent₂elset₃∈ T

(36)

Syntax: Inference Rules

The set ofterms,T is defined by the following rules:

(37)

true∈ T false∈ T 0∈ T

(38)

true∈ T false∈ T 0∈ T t₁∈ T

succt₁∈ T

t₁∈ T predt₁∈ T

t₁∈ T iszerot₁∈ T

(39)

true∈ T false∈ T 0∈ T t₁∈ T

succt₁∈ T

t₁∈ T predt₁∈ T

t₁∈ T iszerot₁∈ T

t₁∈ T t₂∈ T t₃∈ T

ift₁thent₂elset₃∈ T

(40)

Concrete Syntax

S0 = ∅

(41)

Concrete Syntax

S0 = ∅

Si+1 = {true,false,0}

(42)

Concrete Syntax

S0 = ∅

∪ {succt₁,predt₁,iszerot₁|t₁∈ Si}

(43)

Concrete Syntax

S0 = ∅

∪ {ift₁thent₂elset₃|t₁,t₂,t₂∈ Si}

(44)

Concrete Syntax

S0 = ∅

∪ {ift₁thent₂elset₃|t₁,t₂,t₂∈ Si} LetS=S

iSi.

(45)

Concrete Syntax

S0 = ∅

∪ {ift₁thent₂elset₃|t₁,t₂,t₂∈ Si} LetS=S

iSi. Then,T =S.

(46)

Induction on Terms

Anyt∈ T

(47)

Anyt∈ T

Either a ground term, i.e. ∈ {true,false,0}

(48)

Anyt∈ T

Or is created from some smaller terms∈ T

(49)

Anyt∈ T

Allows for inductive definitions and inductive proofs.

(50)

Anyt∈ T

Three sample inductive properties

(51)

Anyt∈ T

Three sample inductive properties Consts(t)

(52)

Anyt∈ T

size(t)

(53)

Anyt∈ T

size(t) depth(t)

(54)

Consts

The set of constants in a term

t

_.

(55)

Consts

t

_.

Consts(true) = {true}

(56)

Consts

t

_.

Consts(false) = {false}

(57)

Consts

t

_.

Consts(0) = {0}

(58)

Consts

t

_.

Consts(0) = {0}

Consts(succt) = Consts(t)

(59)

Consts

t

_.

Consts(0) = {0}

Consts(succt) = Consts(t) Consts(predt) = Consts(t)

(60)

Consts

t

_.

Consts(0) = {0}

Consts(succt) = Consts(t) Consts(predt) = Consts(t) Consts(iszerot) = Consts(t)

(61)

Consts

t

_.

Consts(0) = {0}

Consts(succt) = Consts(t) Consts(predt) = Consts(t) Consts(iszerot) = Consts(t) Consts(ift₁thent₂elset₃) = Consts(t₁)

∪Consts(t₂)

∪Consts(t₃)

(62)

size

The number of nodes in the abstract syntax tree of a term

t

_.

(63)

size

t

_.

size(true) = 1

(64)

size

t

_.

size(true) = 1 size(false) = 1

(65)

size

t

_.

size(true) = 1 size(false) = 1 size(0) = 1

(66)

size

t

_.

size(succt) = size(t) +1

(67)

size

t

_.

size(succt) = size(t) +1 size(predt) = size(t) +1

(68)

size

t

_.

size(succt) = size(t) +1 size(predt) = size(t) +1 size(iszerot) = size(t) +1

(69)

size

t

_.

size(succt) = size(t) +1 size(predt) = size(t) +1 size(iszerot) = size(t) +1

size(ift₁thent₂elset₃) = size(t₁) +size(t₂) +size(t₃)

(70)

depth

The maximum depth of the abstract syntax tree of a term

t

_.

Equivalently, the smallesti such thatt∈ Si.

(71)

depth

t

_.

Equivalently, the smallesti such thatt∈ Si. depth(true) = 1

(72)

depth

t

_.

depth(true) = 1 depth(false) = 1

(73)

depth

t

_.

depth(true) = 1 depth(false) = 1 depth(0) = 1

(74)

depth

t

_.

depth(succt) = depth(t) +1

(75)

depth

t

_.

depth(succt) = depth(t) +1 depth(predt) = depth(t) +1

(76)

depth

t

_.

depth(succt) = depth(t) +1 depth(predt) = depth(t) +1 depth(iszerot) = depth(t) +1

(77)

depth

t

_.

depth(succt) = depth(t) +1 depth(predt) = depth(t) +1 depth(iszerot) = depth(t) +1

depth(ift₁thent₂elset₃) = max(depth(t₁) +depth(t₂) +depth(t₃)) +1

(78)

A Simple Property of Terms

The number of distinct constants in a term

t

is no greater than the size of

t

_.

|Consts(t)| ≤size(t)

(79)

A Simple Property of Terms

The number of distinct constants in a term

t

is no greater than the size of

t

_.

|Consts(t)| ≤size(t) Proof: Exercise.

(80)

The Set of Values

v

_:= _{– values}

(81)

The Set of Values

v

_:= _{– values}

true – value true

(82)

The Set of Values

v

_:= _{– values}

false – value false

(83)

The Set of Values

v

_:= _{– values}

0 – value zero

(84)

The Set of Values

v

_:= _{– values}

0 – value zero

succ

v

– successor value

(85)

Small-step Operational Semantics

t→t^′ denotes “tevaluates tot^′ in one step”

(86)

if true thent₂elset₃→t₂

(87)

if true thent₂elset₃→t₂ if false thent₂elset₃→t₃

(88)

if true thent₂elset₃→t₂ if false thent₂elset₃→t₃

t₁→t^′

1

ift₁thent₂elset₃→ift^′

1thent₂elset₃

(89)

Small-step Operational Semantics (contd. . . )

t₁→t^′

1

succt₁ →succt^′

1

(90)

t₁→t^′

1

pred0→0

(91)

t₁→t^′

1

pred0→0 pred(succv)→v

(92)

t₁→t^′

1

pred0→0 pred(succv)→v

t₁→t^′

1

predt₁ →predt^′

1

(93)

iszero0→true

(94)

iszero0→true iszero(succv)→false

(95)

iszero0→true iszero(succv)→false

t₁→t^′

1

iszerot₁ →iszerot^′

1

(96)

Normal Form

A term istin normal form if no evaluation rule applies to it.

(97)

Normal Form

A term istin normal form if no evaluation rule applies to it.

In other words, there is not^′ such thatt→t^′.

(98)

Evaluation Sequence

An evaluation sequence starting from a termtis a (finite or infinite) sequence of termst₁,t₂, . . ., such that

t→t₁ t₁→t₂ etc.

(99)

Stuck Term

A term is said to bestuckif it is a normal form but not a value.

(100)

Stuck Term

A term is said to bestuckif it is a normal form but not a value.

A simple notion of “run-time type error”