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

Failed to parse (MathML with SVG or PNG fallback (recommended for modern browsers and accessibility tools): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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}}}