Shape Types

Type systems currently available for imperative languages are too weak to detect a significant class of programming errors. For example, they cannot express the property that a list is doubly-linked or circular. We propose a solution to this problem based on a notion of shape types defined as context-free graph grammars. We define graphs in settheoretic terms, and graph modifications as multiset rewrite rules. These rules can be checked statically to ensure that they preserve the structure of the graph specified by the grammar. We provide a syntax for a smooth integration of shape types in C. The programmer can still express pointer manipulations with the expected constant time execution and benefits from the additional guarantee that the property specified by the shape type is an invariant of the program. 1 Motivation and approach Facilities for explicit pointer manipulation are useful for certain classes of applications, but they may lead to a very error-prone style of progra...

• Type: Conference
• Year: 1997
• Where: POPL
• Authors: Pascal Fradet, Daniel Le Métayer
• Keywords: Imperative Languages, POPL 1997, Programming Languages, Shape Type, Type Systems