Z—, an Executable Subset of Z
A description is given of Z—, a computational subset of Z which can be treated as a programming language. The language is presented by taking a small sample specification and taking it through successive refinement stages. After data refinement the specification is in high-level Z--. Operational refinement then takes it into base-level Z--. Auxiliary functions to make Z-- programming easier are described and given formal Z definitions. Z-- itself is a typed functional language, and a sketch is given of how its most important constructs might be interpreted.
KeywordsProgramming Language Auxiliary Function Partial Function Data Refinement Interpretation System
Unable to display preview. Download preview PDF.
Bibliography and References
- E. W. Dijkstra Guarded Commands, Nondeterminacy and the Formal Derivation of Programs CACM, Vol 18, No. 8 (August 1975)Google Scholar
- P. Hudak, S. L. Peyton Jones, P. Wadler Report on the Programming Language Haskell, Version 1.1 Yale University, August 1991Google Scholar
- S. King, I. H. Sørensen, J. Woodcock Z: Grammar and Concrete and Abstract Syntaxes PRG, Oxford University, 1988Google Scholar
- M. Saaltink Z and Eves Technical Report, Odyssey Research Associates, October 1991 (Saaltink also presented a paper at this Z User Meeting, and drew my attention to the above paper, which contains a definition of a function he calls “repeat”, but which is the same as the function which I have called “do”)Google Scholar
- J. M. Spivey The Z Notation–a Reference Manual Prentice Hall, 1989, 1992 (The second edition of the above Manual is to be published shortly after this Z User Meeting. I understand it contains a description of a “let” construction for both expressions and predicates, and of a conditional expression form with “if … then … else … ”. Such features should be well suited for inclusion in the Z— subset, and make its use easier and clearer.)Google Scholar
- G. L. Steele Common Lisp-the Language Digital Press, 1984Google Scholar
- D. Turner An Overview of Miranda Sigplan Notices, Vol 21, No. 12, (December 1986)Google Scholar