UV Manual: Types and Type Checking

Warning

This page is under construction.

Overview

The UV input language is statically strongly typed. Such a scheme was adopted because type information often constitutes valuable safety information about a program.

In the following we describe the types available in the UV language, the subtyping relation on these types, and the rules used when type checking programs and expressions. The grammar rules for types are also available.

Types

Boolean

The boolean type consists of the two constants true and false and the usual operators (boolean connectives) negation !, conjunction /\, disjunction \/, equivalence ==, anti-equivalence (exclusive disjunction) =!=, and implication in both directions ==> and <==.

Finite Range Integers

There are four finite range integer types: cyclic(n) for a positive number n is the type of integers modulo n, bits(n) for positive n is the type of bit vectors of length n (with arithmetic operations performed modulo 2^n), and int(m..n) for integers m and n with m<=n is the type of integers from m up to and including n. There is also the implicit type number(n) of integers, which is used solely for expressions made up from integer literals (such as 3 + 9, which has type number(12)).

Mapping of out-of-range values is done differently for cyclic and bits types on one hand and for int types on the other hand: for the former two values are taken modulo the number of values in the type, whereas for a type int(m..n) values less than m are mapped to m, and values greater than n are mapped to n.

Hence for the declarations

var c: cyclic(8);
var b: bits(3);
var i: int(2..5);

the assignment

c, b, i := 12, 12, 12

results in the validity of the following predicate:

c = 4 /\ b = 4 /\ i = 5

Enumeration Types

An enumeration type is defined by enumerating its domain as an ordered list of identifiers. The ordering of the enumeration induces an order relation on the type with a value a being less than a value b iff a precedes b in the enumeration list.

Record Types

A record type is made up from an unordered series of named fields. Its domain is the unordered tagged Cartesian product of the domains of the field types.

An example of a record type declaration for a record of one boolean component and one cyclic integer component is:

type R = {b: boolean, n: cyclic(7)};

an example of an expression containing a variable r of the above record type is:

r.b /\ r.n != 3

Mapping Types

A mapping type is built from two types, an index type and an element type. Its domain is the set of finite total functions from the index type to the element type. Choosing an integer type as index type yields mappings that correspond to the traditional array types of other languages.

An example of a mapping type declaration for a mapping from the integer interval from 2 to 9, to the record type declared above is:

type M = int(2..9) -> R;

and an example of an expression containing accesses to components of a variable m of the above mapping type (where i is some integer variable) is:

m.4.b /\ m.(i+1).n != 3

Subtyping

In the following we define what it means for a type to be subtype of some type. The subtype notion is important because of the following typing rules:

replacing a subexpression A of type S in an expression by an expression B of type T yields a valid expression if T is a subtype of S,
an assignment A := B in which A is of type S and B is of type T is well-typed if T is a subtype of S.

Note that the above rules are not equivalences (for instance type coercion admits assignments not covered by the second rule).

The binary subtype relation << (read as is subtype of) over types is defined as the reflexive and transitive closure of the smallest relation satisfying the following rules:

int(m..n) << int(p..q) if m>=p and n<=q,
number(m) << cyclic(n),
number(m) << bits(n),
number(m) << int(k..n) if k<=m and n>=m,
{a0: S0, ..., am: Sm} << {b0: T0, ..., bn: Tn} if for each i: 0<=i<=n there is a j such that bi = aj and Sj << Ti.

For instance, boolean is subtype of boolean (and of no other type), int(2..5) is subtype of int(-1..8), and {b: boolean, n: int(2..5)} is subtype of {n: int(-1..8)}.

Type equivalence (as needed for reflexivity) is defined as structural equivalence in which enumeration constants are unique even if they have the same name (as a consequence redefining an enumeration type at an inner scope results in a new type which is not equivalent and not subtype of the outer definition).

Type Checking

A program is well-typed iff the following conditions are met (in this list the term expression refers to top-level expressions, i.e. expressions that are not proper subexpressions of another expression):

all expressions appearing in the program are well-typed,
the types of all expressions in the always section of the program can be coerced to the declared type of the corresponding transparent variable,
all expressions in the initially section of the program are of type boolean,
the types of all right hand side expressions in all statements of the assign section of the program can be coerced to the types of the corresponding left hand side expressions.

An expression is well-typed iff its type can be derived using the following list of rules, in which TYPE[expr] denotes the type of the expression expr:

Warning

The following list is incomplete:

TYPE[true] = boolean for the predefined global symbol true,
TYPE[false] = boolean for the predefined global symbol false,
TYPE[expr] = number(n) for an expression expr built from integer literals only (no variables), where n is the value of the integer expression,
TYPE[var] = T for a declared or transparent variable var where T is its declared type,
TYPE[!expr] = boolean, provided TYPE[expr] = boolean,
TYPE[expr1 op expr2] = boolean for a binary boolean operator op (i.e. one of /\, \/, ==, =!=, ==>, or <==), provided TYPE[expr1] = boolean and TYPE[expr2] = boolean.

Finally, type S can be coerced to type T if one of the following applies:

S is a subtype of T,
S = int(m..n) and T = int(p..q).

The second rule has been added to be able to handle assignments of the form x := x+1 where x is of type int(m..n). According to the typing rules the left hand side is of type int(m..n) whereas the right hand side has type int(m+1..n+1), neither of which is a subtype of the other.

Instead of disallowing such an assignment altogether, it is given the semantics that the value of the right hand side is some value in the target range from m to n in case the value of x+1 is outside this range. The implementation is free to choose that value arbitrarily, no assumption about it can be made.

The rationale behind this semantics is the following: a statement such as the above is quite meaningless in a finite state program, since it corresponds to an explicitly infinite program behavior. The only reasonable occurrence of such an assignment would be guarded by some predicate b that effectively restricts the growth of variable x. The intention should be that in an actual program execution the statement is never enabled in a state in which the right hand side produced an out-of-range value.

In other words, by including an assignment such as x := x + 1 if b in a program, the user actually generates the proof obligation invariant b ==> x<n, which should be checked as a required property of the program.

[Go back to the Language Contents Page] [Go back to the Manual Contents Page]

This page was last updated on 1-Mar-1996.

markus@cs.utexas.edu