Types and invariants in the refinement calculus

AbstractA rigorous treatment of types as sets is given for the refinement calculus, a method of imperative program development. It is simple, supports existing practice, casts new light on type-checking, and suggests generalisations that might be of practical benefit. Its use is illustrated by example