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.