Specifying abstract data types by restriction

Abstract

Restrictions are one instance of mathematically-based relationships between types that can be used to simplify program specifications. Restriction of an abstract data type provides a theoretical justification for the concept of a hidden function that appears in some current specification methodologies. The use of type restrictions to simplify formal specifications is illustrated by the example of traversible stacks.