Shape Checking of Array Programs Authors CBJ and M. Sekanina Abstract Shape theory provides a framework for the study of data types in which shape and data can be manipulated separately. This paper is concerned with shape checking, i.e. the detection of shape errors, such as array bound errors, without handling the data. It can be seen as a form of partial evaluation in which data computations are ignored. It is expressive enough to construct all of the usual array operations. We offer shape theory as a means of reasoning about program structure, and improving object-oriented design.
Values associated with a data type usually have a shape, too.
For example, the shape of a matrix is its size. Shapes, like types, are important in the specification and semantics of programs, and should support tools for static error detection and improved compilation techniques. Tail Recursion through Universal Invariants Author CBJ Abstract Tail recursive constructions suggest a new semantics for datatypes, which allows a direct match between specifications and tail recursive programs. The semantics focusses on loops, their fixpoints, invariants and convergence. Convergent models of the natural numbers and lists are examined in detail, and, under very mild conditions, are shown to be equivalent to the corresponding initial algebra models.