CSCE 314 Lecture 25

« previous | Wednesday, October 26, 2011 | next »

Type Checking

Approximates program evaluation: keeps track that 1+2 evaluates to a number, but not that it equals 3

Type system should be compositional (only a local view of expressions:

if c then t else e

Assume t : T. Then c : Bool and e : T

Formal Description of Type System

Example rules:

• All referenced variables must be declared
• All declared variables must have unique names
• Skip is always valid
• Assignment is valid if
  • Target variable is declared
  • Source expression is valid
  • If variable type is float, then expression is float or int
  • If variable type is int, then expression is int or char
  • Besides general cases, variable must have same type as expression
• Conditional is valid if conditional is Bool and both branches are valid statements
• Loop is valid if condition is Bool and body is a valid statement
• block is valid if all contained statements are valid

Example Mathematical Implementation

${\frac {\Gamma \vdash e:\mathrm {bool} \quad \Gamma \vdash s_{1}\ \mathrm {ok} \quad \Gamma \vdash s_{2}\ \mathrm {ok} }{\Gamma \vdash \mathrm {if} \ e\ s_{1}\ s_{2}\ \mathrm {ok} }}$