An imperative language with read/write type modes
Reading and writing of data is fundamental in computing, as is its control. However control of reading and writing has traditionally only been available at the level of file systems, and not programming language data structures. In this paper a simple imperative language is described which uses type modes to control reading and writing of data. A type may be labelled read-write or read-only; a read-only type is guaranteed by the type system not to be written. Furthermore a read-write type may be treated read-only in a sub-context. To achieve this implicit aliasing is prevented and the program heap is partitioned into collections. Collections form a unit of read-write control of heap allocated data, by isolating different heap regions. Collections were originally introduced in the Euclid and Turing programming languages for abasing control; however this was rather restrictive and not strictly enforced. Controlling aliasing is beneficial in its own right since abasing is a common source of programming errors.
KeywordsType Mode List Length Formal Collection Abstract Syntax Type Check
Unable to display preview. Download preview PDF.
- 1.P G Bancroft and I J Hayes. Refinement in a type extension context.In Proceedings of the Fifth Australian Refinement Workshop (ARW-96). Department of Computer Science, The University of Queensland, April 1996.Google Scholar
- 2.D Gifford, P Jouvelot, M Sheldon, and J O'Toole. Report on the FX-91 programming language. Technical Report TR-531 (revised version), LCS, MIT.Google Scholar
- 3.D K Gifford and J M Lucassen. Integrating functional and imperative programming. In ACM Conference on Lisp and Functional Programming, pages 28–38, 1986.Google Scholar
- 4.J-Y Girard. Linear logic. Theoretical Computing Science, (50):1–102, 1987.Google Scholar
- 5.J Hogg. Islands: Aliasing Protection in Object Oriented Languages. In OOPSLA'91, pages 271–285, 1991.Google Scholar
- 6.R C Holt and J R Cordy. The Turing Programming Language. CACM 31(12):1410–1423, 1988.Google Scholar
- 7.R C Holt, P A Matthews, J A Rosselet, and J R Cordy. The Turing Language: Design and Definition. Prentice Hall, 1987.Google Scholar
- 8.S L Peyton Jones and J Launchbury. State in Haskell. LASC, 8(5):293–341, December 1995.Google Scholar
- 9.G J Popek, J J Horning, B W Lampson, J G Mitchell, and R L London. Notes on the Design of Euclid. ACM SIGPLAN Notices, 12(3), 1977.Google Scholar
- 10.J C Reynolds. Syntactic control of interference. In 5th ACM Symposium on Principles of Programming Languages, pages 39–46, 1978.Google Scholar
- 11.R E Strom and S Yemini. Typestate a programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering, SE12(1):157–171, January 1986.Google Scholar