×

A mode system for flexible alias protection. (English) Zbl 0924.68038

Grundy, Jim (ed.) et al., International refinement workshop and formal methods Pacific 1998. Proceedings of IRW/FMP ’98. Canberra, Australia, September 29 - October 2, 1998. Berlin: Springer. Springer Series in Discrete Mathematics and Theoretical Computer Science. 306-323 (1998).
Summary: Object-oriented programming languages allow inter-object aliasing to represent linked data structures and networks of interacting objects. Aliasing complicates formal reasoning about programs, as it can occur anywhere in a program. In our mode system programs are annotated with modes that indicate object ownership and control the extent of object aliases. By localising aliases, our mode system provides a context for formal reasoning about object systems. Being statically checkable our system offers a practical target for the formal refinement of object-based specifications.
For the entire collection see [Zbl 0910.00058].

MSC:

68N15 Theory of programming languages

Software:

Virginity
PDF BibTeX XML Cite