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.
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