Bibliography

[Arnold-Gosling-Holmes00]

Ken Arnold, James Gosling, and David Holmes. The Java Programming Language Third Edition. The Java Series. Addison-Wesley, Reading, MA, 2000.

[America87]

Pierre America. Inheritance and subtyping in a parallel object-oriented language. In Jean Bezivin et al., editors, ECOOP '87, European Conference on Object-Oriented Programming, Paris, France, pages 234--242, New York, NY, June 1987. Springer-Verlag. Lecture Notes in Computer Science, volume 276.

[America91]

Pierre America. Designing an object-oriented programming language with behavioural subtyping. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, REX School/Workshop, Noordwijkerhout, The Netherlands, May/June 1990, volume 489 of Lecture Notes in Computer Science, pages 60--90. Springer-Verlag, New York, NY, 1991.

[Back88]

R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25(6):593--624, August 1988.

[Back-vonWright89a]

R. J. R. Back and J. von Wright. Refinement Calculus, Part I: Sequential Nondeterministic Programs. In J. W. de Bakker, et al, (eds.), Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Netherlands, May/June 1989, pages 42-66. Volume 430 of Lecure Notes Computer Science, Spring-Verlag, 1989.

[Back-Mikhajlova-vonWright98]

Ralph Back, Anna Mikhajlova, and Joakim von Wright. Modeling component environments and interactive programs using iterative choice. Technical Report 200, Turku Centre for Computer Science, September 1998.
`http://www.tucs.abo.fi/publications/techreports/TR200.html'.

[Back-vonWright98]

Ralph-Johan Back and Joakim von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.

[Beck-Gamm98]

Kent Beck and Erich Gamma. Test infected: Programmers love writing tests. Java Report, 3(7), July 1998.

[Buechi-Weck00]

Martin Büchi and Wolfgang Weck. The Greybox Approach: When Blackbox Specifications Hide Too Much. Technical Report 297, Turku Centre for Computer Science, August 1999.
`http://www.tucs.abo.fi/publications/techreports/TR297.html'.

[Borgida-Mylopoulos-Reiter95]

Alex Borgida, John Mylopoulos, and Raymond Reiter. On the frame problem in procedure specifications. IEEE Transactions on Software Engineering, 21(10):785--798, October 1995.

[Chalin02]

Back to Basics: Language Support and Semantics of Basic Infinite Integer Types in JML and Larch Technical Report CU-CS 2002-003.2, Computer Science Department, Concordia University, October 2002. Updated March 2003, which is available from the URL
`http://www.cs.concordia.ca/~chalin/papers/TR-2002-003.pdf'.

[Chalin04]

Patrice Chalin. JML Support for Primitive Arbitrary Precision Numeric Types: Definition and Semantics. Journal of Object Technology, 3(6):57-79, June 2004.

[Cheon03]

Yoonsik Cheon. A runtime assertion checker for the Java Modeling Language. Technical Report 03-09, Department of Computer Science, Iowa State University, Ames, IA, April 2003. The author's Ph.D. dissertation, which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR03-09/TR.pdf'.

[Cheon-Leavens02]

Yoonsik Cheon and Gary T. Leavens. A Simple and Practical Approach to Unit Testing: The JML and JUnit Way. In ECOOP 2002 -- Object-Oriented Programming, 16th European Conference, Malaga, Spain, pages 231--255. Springer-Verlag, June 2002. Also Department of Computer Science, Iowa State University, TR #01-12a, November 2001, revised March 2002 which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR01-12/TR.pdf'.

[Cheon-Leavens02b]

Yoonsik Cheon and Gary T. Leavens. A Runtime Assertion Checker for the Java Modeling Language (JML). In Hamid R. Arabnia and Youngsong Mun (eds.), Proceedings of the International Conference on Software Engineering Research and Practice (SERP '02), Las Vegas, Nevada, USA, pages 322--328. CSREA Press, June 2002. Also Department of Computer Science, Iowa State University, TR #02-05, March 2002 which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR02-05/TR.pdf'.

[Cheon-Leavens05]

Yoonsik Cheon and Gary T. Leavens. A contextual interpretation of undefinedness for runtime assertion checking. In AADEBUG 2005, Proceedings of the Sixth International Symposium on Automated and Analysis-Driven Debugging, Monterey, California, September 19--21, 2005, pages 149--157. ACM Press, September 2005.

[Cohen90]

Edward Cohen. Programming in the 1990s: An Introduction to the Calculation of Programs. Springer-Verlag, New York, N.Y., 1990.

[Chalin02]

Patrice Chalin. Back to Basics: Language Support and Semantics of Basic Infinite Integer Types in JML and Larch. Computer Science Department, Concordia University, Technical Report CU-CS 2002-003.1. Available in `http://tinyurl.com/e5q6g', October, 2002.

[Dhara-Leavens96]

Krishna Kishore Dhara and Gary T. Leavens. Forcing behavioral subtyping through specification inheritance. In Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pages 258--267. IEEE Computer Society Press, March 1996. An extended version is Department of Computer Science, Iowa State University, TR #95-20b, December 1995, which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR95-20/TR.ps.Z'.

[Ernst-etal01]

Michael D. Ernst, Jake Cockrell, William G. Griswold, and David Notkin Dynamically Discovering Likely Program Invariants to Support Program Evolution IEEE Transactions on Software Engineering, 27(2):1--25, February 2001.

[Finney96]

Kate Finney. Mathematical notation in formal specification: Too difficult for the masses? IEEE Transactions on Software Engineering, 22(2):158--159, February 1996.

[Fitzgerald-Larsen98]

John Fitzgerald and Peter Gorm Larsen. Modelling Systems: Practical Tools and Techniques in Software Development. Cambridge University Press, Cambridge, UK, 1998.

[Gifford-Lucassen86]

David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In ACM Conference on LISP and Functional Programming, pages 28--38. ACM, August 1986.

[Gosling-Joy-Steele96]

James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. The Java Series. Addison-Wesley, Reading, MA, 1996.

[Gosling-etal00]

James Gosling, Bill Joy, Guy Steele, and Gilad Bracha. The Java Language Specification Second Edition. The Java Series. Addison-Wesley, Boston, MA, 2000.

[Gries-Schneider95]

David Gries and Fred B. Schneider. Avoiding the Undefined by Underspecification. In Jan van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 366--373. Springer-Verlag, New York, N.Y., 1995.

[Guttag-Horning93]

John V. Guttag, James J. Horning, S.J. Garland, K.D. Jones, A. Modet, and J.M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag, New York, N.Y., 1993.

[Hayes93]

I. Hayes, editor. Specification Case Studies. International Series in Computer Science. Prentice-Hall, Inc., second edition, 1993.

[Hoare69]

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--583, October 1969.

[Hoare72a]

C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271--281, 1972.

[Huisman01]

Marieke Huisman. Reasoning about JAVA programs in higher order logic with PVS and Isabelle. IPA dissertation series, 2001-03. Ph.D. dissertation, University of Nijmegen, 2001.

[ISO96]

International Standards Organization. Information Technology - Programming Languages, Their Environments and System Software Interfaces - Vienna Development Method - Specification Language - Part 1: Base language. International Standard ISO/IEC 13817-1, December, 1996.

[Jacobs-etal98]

Bart Jacobs, Joachim van den Berg, Marieke Huisman Martijn van Berkum, Ulrich Hensel, and Hendrik Tews. Reasoning about Java Classes (Preliminary Report). In OOPSLA '98 Conference Proceedings, volume 33, number 10 of ACM SIGPLAN Notices, pages 329--340. October 1998.

[Jones90]

Cliff B. Jones. Systematic Software Development Using VDM. International Series in Computer Science. Prentice Hall, Englewood Cliffs, N.J., second edition, 1990.

[Jonkers91]

H. B. M. Jonkers. Upgrading the pre- and postcondition technique. In S. Prehn and W. J. Toetenel, editors, VDM '91 Formal Software Development Methods 4th International Symposium of VDM Europe Noordwijkerhout, The Netherlands, Volume 1: Conference Contributions, volume 551 of Lecture Notes in Computer Science, pages 428--456. Springer-Verlag, New York, N.Y., October 1991.

[Lano-Haughton94]

K. Lano and H. Haughton, editors. Object-Oriented Specification Case Studies. The Object-Oriented Series. Prentice Hall, New York, N.Y., 1994.

[Leavens96b]

Gary T. Leavens. An overview of Larch/C++: Behavioral specifications for C++ modules. In Haim Kilov and William Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, chapter 8, pages 121--142. Kluwer Academic Publishers, Boston, 1996. An extended version is TR #96-01d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011.

[Leavens97c]

Gary T. Leavens. Larch/C++ Reference Manual. Version 5.14. Available in
`http://www.eecs.ucf.edu/~leavens/larchc++.html', October 1997.

[LeavensLarchFAQ]

Gary T. Leavens. Larch frequently asked questions. Version 1.110. Available in `http://www.eecs.ucf.edu/~leavens/larch-faq.html', May 2000.

[Leavens-etal-JMLRef]

Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, and Joseph Kiniry. JML Reference Manual. Available from `http://www.jmlspecs.org/'.

[Leavens-Baker99]

Gary T. Leavens and Albert L. Baker. Enhancing the pre- and postcondition technique for more expressive specifications. In Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors, FM'99 -- Formal Methods: World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 1999, Proceedings, volume 1709 of Lecture Notes in Computer Science, pages 1087--1106. Springer-Verlag, 1999.

[Leavens-Baker-Ruby99]

Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: a Notation for Detailed Design. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications for Businesses and Systems, chapter 12, pages 175-188.

[Leavens-Weihl95]

Gary T. Leavens and William E. Weihl. Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica, 32(8):705--778, November 1995.

[Leavens-Wing97a]

Gary T. Leavens and Jeannette M. Wing. Protective interface specifications. In Michel Bidoit and Max Dauchet, editors, TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, volume 1214 of Lecture Notes in Computer Science, pages 520--534. Springer-Verlag, New York, N.Y., 1997.

[Ledgard80]

Henry. F. Ledgard. A human engineered variant of BNF. ACM SIGPLAN Notices, 15(10):57--62, October 1980.

[Leino95a]

K. Rustan M. Leino. A myth in the modular specification of programs. Technical Report KRML 63, Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301, November 1995. Obtain from the author, at leino@microsoft.com.

[Leino95]

K. Rustan M. Leino. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, 1995. Available as Technical Report Caltech-CS-TR-95-03.

[Leino98]

K. Rustan M. Leino. Data groups: Specifying the modification of extended state. In OOPSLA '98 Conference Proceedings, pp. 144-153. Volume 33, number 10 of ACM SIGPLAN Notices, October, 1998.

[Leino-Nelson-Saxe00]

K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC/Java User's Manual. Compaq SRC Technical Note 2000-02, October, 2000.

[Leino-Poetzsch-Heffter-Zhou02]

Using Data Groups to Specify and Check Side Effects. Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI '02), pp. 246-257. Volume 37, number 5 of ACM SIGPLAN Notices, June, 2002.

[Leino-etal00]

K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended Static Checking. Web page at
`http://research.compaq.com/SRC/esc/Esc.html'.

[Lerner91]

Richard Allen Lerner. Specifying objects of concurrent systems. Ph.D. Thesis CMU-CS-91-131, School of Computer Science, Carnegie Mellon University, May 1991.

[Liskov-Wing94]

Barbara Liskov and Jeannette Wing. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811--1841, November 1994.

[Lucassen87]

John M. Lucassen. Types and effects: Towards the integration of functional and imperative programming. Technical Report TR-408, Massachusetts Institute of Technology, Laboratory for Computer Science, August 1987.

[Lucassen-Gifford88]

John M. Lucassen and David K. Gifford. Polymorphic effect systems. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, San Diego, Calif., pages 47--57. ACM, January 1988.

[Luckham-vonHenke85]

David Luckham and Friedrich W. von Henke. An overview of Anna - a specification language for Ada. IEEE Software, 2(2):9--23, March 1985.

[Luckham-etal87]

David Luckham, Friedrich W. von Henke, Bernd Krieg-Brückner, and Olaf Owe. ANNA - A Language for Annotating Ada Programs, volume 260 of Lecture Notes in Computer Science. Springer-Verlag, New York, N.Y., 1987.

[Meyer92a]

Bertrand Meyer. Applying "design by contract". Computer, 25(10):40--51, October 1992.

[Meyer92b]

Bertrand Meyer. Eiffel: The Language. Object-Oriented Series. Prentice Hall, New York, N.Y., 1992.

[Meyer97]

Bertrand Meyer. Object-oriented Software Construction. Prentice Hall, New York, N.Y., second edition, 1997.

[Morgan94]

Carroll Morgan. Programming from Specifications: Second Edition. Prentice Hall International, Hempstead, UK, 1994.

[Morgan-Vickers94]

Carroll Morgan and Trevor Vickers, editors. On the refinement calculus. Formal approaches of computing and information technology series. Springer-Verlag, New York, N.Y., 1994.

[Morris87]

Joseph M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287--306, December 1987.

[Mueller02]

Peter Müller. Modular Specification and Verification of Object-Oriented Programs. Volume 2262 of Lecture Notes in Computer Science, Springer-Verlag, 2002.

[Nielson-Nielson-Amtoft97]

H. R. Nielson, F. Nielson, and T. Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In M. Dam, editor, Proceedings of the Fifth LOMAPS Workshop, number 1192 in Lecture Notes in Computer Science. Springer-Verlag, 1997.

[Ogden-etal94]

William F. Ogden, Murali Sitaraman, Bruce W. Weide, and Stuart H. Zweben. Part I: The RESOLVE framework and discipline -- a research synopsis. ACM SIGSOFT Software Engineering Notes, 19(4):23--28, Oct 1994.

[Owre-etal95]

Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107--125, February 1995.

[Poll-Jacobs00]

E. Poll and B.P.F. Jacobs. A Logic for the Java Modeling Language JML. Computing Science Institute Nijmegen, Technical Report CSI-R0018. Catholic University of Nijmegen, Toernooiveld 1, 6525 ED Nijmegen, November 2000.

[Poetzsch-Heffter97]

Arnd Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, January 1997.

[Raghavan-Leavens05]

Arun D. Raghavan and Gary T. Leavens. Desugaring JML Method Specifications. Technical Report 00-03e, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, revised May 2005. Available in
`ftp://ftp.cs.iastate.edu/pub/techreports/TR00-03/TR.ps.gz'.

[Rosenblum95]

David S. Rosenblum. A practical approach to programming with assertions. IEEE Transactions on Software Engineering, 21(1):19--31, January 1995.

[Ruby-Leavens00]

Clyde Ruby and Gary T. Leavens. Safely Creating Correct Subclasses without Seeing Superclass Code. In OOPSLA 2000 Conference on Object-Oriented Programming, Systems, Languages, and Applications, Minneapolis, Minnesota, pp. 208-228. Volume 35, number 10 of ACM SIGPLAN Notices, October, 2000. Also technical report 00-05d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011. April 2000, revised April, June, July 2000. Available in
`ftp://ftp.cs.iastate.edu/pub/techreports/TR00-05/TR.ps.gz'.

[Salcianu-Rinard05]

Alexandru Salcianu and Martin Rinard. Purity and Side Effect Analysis for Java Programs. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation. Paris, France January 2005. Available in
`http://www.mit.edu/~salcianu/publications/vmcai05-purity.pdf'

[Sivaprasad95]

Gowri Sivaprasad. Larch/CORBA: Specifying the behavior of CORBA-IDL interfaces. Technical Report 95-27a, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, December 1995.

[Spivey92]

J. Michael Spivey. The Z Notation: A Reference Manual. International Series in Computer Science. Prentice-Hall, New York, N.Y., second edition, 1992.

[Talpin-Jouvelot94]

Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 111(2):245--296, June 1994.

[Tan94]

Yang Meng Tan. Interface language for supporting programming styles. ACM SIGPLAN Notices, 29(8):74--83, August 1994. Proceedings of the Workshop on Interface Definition Languages.

[Tan95]

Yang Meng Tan. Formal Specification Techniques for Engineering Modular C Programs, volume 1 of Kluwer International Series in Software Engineering. Kluwer Academic Publishers, Boston, 1995.

[Wahls-Leavens-Baker00]

Tim Wahls, Gary T. Leavens, and Albert L. Baker. Executing Formal Specifications with Concurrent Constraint Programming. Automated Software Engineering, 7(4):315-343, December, 2000.

[Watt91]

David A. Watt. Programming Language Syntax and Semantics. Prentice Hall International Series in Computer Science. Prentice-Hall, New York, N.Y., 1991.

[Whitehead-Russell25]

A. N. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, London, second edition. edition, 1925.

[Wills94]

Alan Wills. Refinement in Fresco. In Lano and Houghton [Lano-Haughton94], chapter 9, pages 184--201.

[Wing87]

Jeannette M. Wing. Writing Larch interface language specifications. ACM Transactions on Programming Languages and Systems, 9(1):1--24, January 1987.

[Wing90a]

Jeannette M. Wing. A specifier's introduction to formal methods. Computer, 23(9):8--24, September 1990.

[Wing83]

Jeannette Marie Wing. A two-tiered approach to specifying programs. Technical Report TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science, 1983.

[Woodcock-Davies96]

Jim Woodcock and Jim Davies. Using Z: Specification, Refinement, and Proof. Prentice Hall, International Series in Computer Science, 1996.

[Wright92]

Andrew K. Wright. Typing references by effect inference. In Bernd Krieg-Bruckner, editor, ESOP '92, 4th European Symposium on Programming, Rennes, France, February 1992, Proceedings, volume 582 of Lecture Notes in Computer Science, pages 473--491. Springer-Verlag, New York, N.Y., 1992.