A. Bibliography

[Abramson and Dahl 1989]

Harvey Abramson and Veronica Dahl. Logic Grammars. Symbolic Computation series. Springer Verlag, 1989.

[Aho and Ullman 1977]

Alfred V. Aho and Jeffrey D. Ullman. Principles of Compiler Design. Addison-Wesley, 1977.

[Aho et al. 1988]

Alfred V. Aho, Brian W. Kernighan, and Peter J. Weinberger. The AWK Programming Language. Addison-Wesley, 1988.

[Allison 1986]

L. Allison. A Practical Introduction to Denotational Semantics. Cambridge University Press, 1986.

[Andrews et al. 1991]

Derek J. Andrews, Don Ward, Roger Henry, et al. CD10514-2(draft):1991 fourth working draft Modula-2 standard, 1991.

[Austin 1976]

J. L. Austin. How to do Things with Words. Oxford University Press, 2nd edition, 1976.

[Bergeretti and Carré 1985]

J. F. Bergeretti and B. Carré. Information flow and data flow analysis of while programs. ACM Transactions on Programming Languages and Systems, 7:37--61, 1985.

[Bramson 1984]

B. D. Bramson. Malvern's program analysers. RSRE Research Review, 1984.

[Carré 1989]

Bernard A. Carré. Reliable programming in standard languages. In Chris T. Sennett, editor. High-integrity Software. Pitman, 1989.

[Clocksin and Mellish 1987]

W. F. Clocksin and C. S. Mellish. Programming in Prolog. Springer Verlag, 3rd edition, 1987.

[Cohn 1979]

Avra J. Cohn. Machine Assisted Proofs of Recursion Implementation. PhD thesis, University of Edinburgh, 1979.

[Cousot and Cousot 1977]

Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static ana lysis of programs by construction or approximation of fixed points. In Proceedings of the Fourth Annual ACM Symposium on the Principles of Programming Languages. ACM, 1977.

[De Millo et al. 1979]

R. A. De Millo, R. J. Lipton, and A. J. Perlis. Social processes and proofs of theorems and programs. Communications of the ACM, 22(5):271--280, 1979. see also 'ACM Forum', 22(11):621--630.

[Gordon 1979]

Michael J. C. Gordon. The Denotational Description of Programming Languages---An Introduction. Springer Verlag, 1979.

[Hall 1990]

J. Anthony Hall. Seven myths of formal methods. IEEE Software, pages 21--28, September 1990.

[Hayes 1987]

Ian Hayes. Specification Case Studies. Prentice Hall, 1987.

[Hoare 1991]

C. A. R. Hoare. Refinement algebra proves correctness of compiling specifications. In C. Carroll Morgan and James C. P. Woodcock, editors, 3rd BCS-FACS Refinement Workshop, Workshops in Computing, pp 33--48. Springer-Verlag, 1991.

[Hoare and Jones 1989]

C. A. R. Hoare and Cliff B. Jones. Essays in Computer Science. Prentice Hall, 1989.

[Kernighan and Pike 1984]

Brian W. Kernighan and Rob Pike. The Unix Programming Environment. Prentice Hall, 1984.

[Knuth 1968]

Donald E. Knuth. Semantics of context-free languages. Mathematical Systems Theory, 2(2):127--145, 1968. correction, 5(1):95--96, 1971.

[Lee 1989]

Peter Lee. Realistic Compiler Generation. Foundations of Computing series. MIT Press, 1989.

[McCarthy and Painter 1966]

J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. Technical Report AIM-40, Stanford University, 1966.

[Meyer 1985]

Bertrand Meyer. On formalism in specifications. IEEE Software, 2:6--26, January 1985.

[Meyer 1990]

Bertrand Meyer. Introduction to the Theory of Programming Languages. Prentice Hall, 1990.

[Milner and Weyhrauch 1972]

Robin Milner and R. Weyhrauch. Proving compiler correctness in a mechanized logic. Machine Intelligence, 7, 1972.

[Morris 1973]

F. L. Morris. Advice on structuring compilers and proving them correct. In Proceedings of the First Annual ACM Symposium on Principles of Programming Languages, pages 144--152. ACM, 1973.

[Mosses 1975]

Peter D. Mosses. Mathematical Semantics and Compiler Generation. PhD thesis, University of Oxford, 1975.

[Neumann 1985]

Peter G. Neumann. Some computer-related disasters and other egregious horrors. ACM SIGSOFT Software Engineering Notes, 10(1):6, 1985.

[Parker 1991]

Colin E. Parker. Z tools catalogue. ZIP document ZIP/BAe/90/020, British Aerospace, Warton, May 1991.

[Paulson 1981]

L. Paulson. A Compiler Generator for Semantic Grammars. PhD thesis, Stanford University, 1981.

[Paulson 1982]

L. Paulson. A semantics-directed compiler generator. In Proceedings of the Ninth Annual ACM Symposium on Principles of Programming Languages, pages 224--239. ACM, 1982.

[Polak 1981]

Wolfgang Polak. Compiler Specification and Verification, volume 124 of Lecture Notes in Computer Science. Springer Verlag, 1981.

[Potter et al. 1991]

Ben Potter, Jane Sinclair, and David Till. An Introduction to Formal Specification and Z. Prentice Hall, 1991.

[Schmidt 1988]

David A. Schmidt. Denotational Semantics: A Methodology for Language Development. Wm. C. Brown Publishers, 1988.

[Spivey 1992]

J. Michael Spivey. The Z Notation: a Reference Manual. Prentice Hall, 2nd edition, 1992.

[Stepney and Lord 1987]

Susan Stepney and Stephen P. Lord. Formal specification of an access control system. Software---Practice and Experience, 17(9):575--593, 1987.

[Stepney et al. 1991]

Susan Stepney, Dave Whitley, David Cooper, and Colin Grant. A demonstrably correct compiler. BCS Formal Aspects of Computing, 3:58--101, 1991.

[Sterling and Shapiro 1986]

Leon Sterling and Ehud Shapiro. The Art of Prolog: Advanced Programming Techniques. MIT Press, 1986.

[Stoy 1977]

Joseph E. Stoy. Denotational Semantics and the Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.

[Tennent 1991]

R. D. Tennent. Semantics of Programming Languages. Prentice Hall, 1991.

[Tofte 1990]

Mads Tofte. Compiler Generators: what they can do, what they might do, and what they will probably never do, volume 19 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1990.

[Wand 1984]

M. Wand. A semantic prototyping system. Proceedings of the SIGPLAN 84 Symposium on Compiler Construction; ACM SIGPLAN Notices, 19(6):213--221, 1984.

[Warren 1980]

David H. Warren. Logic programming and compiler writing. Software---Practice and Experience, 10:97--125, 1980.

[Woodcock and Brien 1992]

James C. P. Woodcock and Stephen M. Brien. W: A logic for Z. In John E. Nicholls, editor. Proceedings of the 6th Annual Z User Meeting, York 1991, Workshops in Computing. Springer Verlag, 1992.