Specification and synthesis of bounded indirection

摘要

Bounded indirection is a restricted form of pointers, for system specification. It provides a mechanism for compact descriptions of many complex control structures, such as interrupts, continuations, and dynamic connections between machines. We describe three kinds of indirection-control state, value and net indirection-for use in different aspects of system description. Transformations on indirection representations and methods for synthesizing bounded indirection within the framework of behavior tables are presented.