Shape Types

13 years 8 months ago

Download pop-art.inrialpes.fr

Type systems currently available for imperative languages are too weak to detect a signiﬁcant 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 deﬁned as context-free graph grammars. We deﬁne graphs in settheoretic terms, and graph modiﬁcations as multiset rewrite rules. These rules can be checked statically to ensure that they preserve the structure of the graph speciﬁed 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 beneﬁts from the additional guarantee that the property speciﬁed 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...

Pascal Fradet, Daniel Le Métayer

Real-time Traffic