State Types


A state type is a mapping that associates variables with viewtypes. Intuitively, if a program point can be assigned a state type ST, then each variable in the domain of ST must have the type with which ST associates the variable when program execution reaches that point. In ATS, a state type is represented as follows:

(x_1 : VT_1, ..., x_n : VT_n)
where for 1 <= i <= n, each variable x_i is assiciated with the viewtype VT_i.

The code used for illustration is available here.