Bibliography

[America87]

Pierre America. Inheritance and Subtyping in a Parallel Object-Oriented Language. In Jean Bezivin and others (eds.), ECOOP '87, European Conference on Object-Oriented Programming, Paris, France. Lecture Notes in Computer Science, Vol. 276 (Springer-Verlag, NY), pages 234-242.

[Arnold-Gosling-Holmes00]

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

[ANSI95]

Working Paper for Draft Proposed International Standard for Information Systems -- Programming Language C++. CBEMA, 1250 Eye Street NW, Suite 200, Washington DC 20005, April 28, 1995. (Obtained by anonymous ftp to research.att.com, directory dist/c++std/WP.)

[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 Lecture Notes Computer Science, Spring-Verlag, 1989.

[Back-vonWright98]

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

[Borgida-etal95]

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.

[Boyland00]

John Boyland. Alias burying: Unique variables without destructive reads. Software--Practice and Experience, 31(6):533-553, May 2001.

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

[Buechi00]

Martin Büchi. Safe Language Mechanisms for Modularization and Concurrency. Ph.D. Thesis, Turku Center for Computer Science, May 2000. TUCS Dissertations No. 28.

[Burdy-etal03]

Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. Dept. of Computer Science, University of Nijmegen, TR NIII-R0309, 2003.
`http://www.eecs.ucf.edu/~leavens/JML/OldReleases/jml-white-paper.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. Available from
`http://www.jot.fm/issues/issue_2004_06/article3'

[Chalin07]

Patrice Chalin. A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler. Proceedings of the International Conference on Software Engineering (ICSE), Minneapolis, MN, USA, 2007.

[Chalin-Rioux05]

Patrice Chalin and Frederic Rioux. Non-null References by Default in the Java Modeling Language. In Proceedings of the Workshop on the Specification and Verification of Component-Based Systems (SAVCBS'05), Lisbon, Portugal. September, 2005. An updated version is available as Department of Computer Science, Concordia University, ENCS-CSE TR 2005-004, December 2005, which is available from the URL
`http://www.cs.concordia.ca/~chalin/papers/TR-2005-004-r3.2.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-etal05]

Yoonsik Cheon, Gary T. Leavens, Murali Sitaraman, and Stephen Edwards. Model Variables: Cleanly Supporting Abstraction in Design By Contract. Software--Practice and Experience, 35(6):583-599, May 2005. Also Department of Computer Science, Iowa State University, TR 03-10, March 2003.
`ftp://ftp.cs.iastate.edu/pub/techreports/TR03-10/TR.pdf'.

[Cheon03]

Yoonsik Cheon. A Runtime Assertion Checker for the Java Modeling Language. Department of Computer Science, Iowa State University, TR 03-09, April, 2003.
`ftp://ftp.cs.iastate.edu/pub/techreports/TR03-09/TR.pdf'

[Cohen90]

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

[Corbett-etal00]

James C. Corbett, Matthew B. Dwyer, John Hatcliff, Shawn Laubach, Corina S. Pasareanu, Robby, and Hongjun Zheng. Bandera: Extracting Finite-State Models from Java Source Code. In S. Brookes and M. Main and A. Melton and M. Mislove (eds.), Proceedings of the 22nd International Conference on Software Engineering, pp. 439-448, ACM Press, 2000.

[Dhara-Leavens96]

Krishna Kishore Dhara and Gary T. Leavens. Forcing Behavioral Subtyping Through Specification Inheritance. In Proceedings 18th International Conference on Software Engineering, Berlin, Germany, pages 258-267. IEEE 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'.

[Dietl-Drossopoulou-Mueller07]

Werner Dietl, Sophia Drossopoulou and Peter Müller. Generic Universe Types. In E. Ernst, editor, European Conference on Object-Oriented Programming (ECOOP) pages 28--53, 2007. Available from
`http://sct.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=DietlDrossopoulouMueller07a.pdf'.

[Dietl-Mueller04]

Werner Dietl and Peter Müller. Exceptions in ownership type systems. In E. Poll, editor, Formal Techniques for Java-like Programs pages 49--54, 2004. Available from
`http://sct.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=DietlMueller04.pdf'.

[Dietl-Mueller05]

Werner Dietl and Peter Müller. Universes: Lightweight Ownership for JML. Journal of Object Technology, 4(8):5--32, October 2005. Available from
`http://www.jot.fm/issues/issue_2005_10/article1.pdf'.

[Dietl-Mueller-Schregenberger08]

Werner Dietl, Peter Müller and Daniel Schregenberger. Universe Type System -- Quick-Reference. Available from
`http://sct.inf.ethz.ch/research/universes/tools/juts-quickref.pdf'.

[Dijkstra76]

Edsger W. Dijkstra. A Discipline of Programming (Prentice-Hall, Englewood Cliffs, N.J., 1976).

[Edwards-etal94]

Stephen H. Edwards, Wayne D. Heym, Timothy J. Long, Murali Sitaraman, and Bruce W. Weide. Part II: Specifying Components in RESOLVE. ACM SIGSOFT Software Engineering Notes, 19(4):29-39, October 1994.

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

[Fitzgerald-Larsen98]

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

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

[Gosling-etal05]

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

[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-Horning-Wing85b]

John V. Guttag and James J. Horning and Jeannette M. Wing. The Larch Family of Specification Languages. IEEE Software, 2(5):24-36, September 1985.

[Guttag-Horning93]

John V. Guttag and James J. Horning with S.J. Garland, K.D. Jones, A. Modet and J.M. Wing. Larch: Languages and Tools for Formal Specification (Springer-Verlag, NY, 1993).

[Hall90]

Anthony Hall. Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990.

[Hayes93]

I. Hayes (ed.), Specification Case Studies, second edition (Prentice-Hall, Englewood Cliffs, N.J., 1990).

[Hesselink92]

Wim H. Hesselink. Programs, Recursion, and Unbounded Choice (Cambridge University Press, Cambridge, UK, 1992).

[Hoare69]

C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Comm. 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.

[Khurshid-Marinov-Jackson02]

Sarfraz Khurshid and Darko Marinov and Daniel Jackson. An Analyzable Annotation Language. In Proceedings of OOPSLA '02 Conference on Object-Oriented Programming, Languages, Systems, and Applications. (ACM SIGPLAN Notices, 37(11):231--245, October 2002).

[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 Proceedings (ACM SIGPLAN Notices, 33(10):329-490, 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.

[Jones95e]

C.B. Jones, Partial functions and logics: A warning. Information Processing Letters, 54(2):65-67, 1995.

[Kiczales-Lamping92]

Gregor Kiczales and John Lamping. Issues in the Design and Documentation of Class Libraries. In Andreas Paepcke (ed.), OOPSLA '92 Proceedings (ACM SIGPLAN Notices, 27(10):435-451, October 1992).

[Kiniry-Cok04]

Joseph R. Kiniry and David R. Cok. ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2 and a report on a case study involving the use of ESC/Java2 to verify portions of an Internet voting tally system. In Marieke Huisman (ed.), CASSIS 2004 - Construction and Analysis of Safe, Secure and Interoperable Smart devices, Marseille, France, 2004, Proceedings, volume 3362 of Lecture Notes in Computer Science, pages 108-128. Springer-Verlag, 2004.

[Krone-Ogden-Sitaraman03]

Joan Krone, William F. Ogden, Murali Sitaraman. Modular Verification of Performance Constraints. Technical Report RSRG-03-04, Department of Computer Science, Clemson University, May, 2003. Available from `http://www.cs.clemson.edu/~resolve/reports/RSRG-03-04.pdf'

[Lamport89]

Leslie Lamport. A Simple Approach to Specifying Concurrent Systems. CACM, 32(1):32-45, January 1989.

[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-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-Baker-Ruby06]

Gary T. Leavens, Albert L. Baker, and Clyde Ruby. Preliminary Design of JML: A Behavioral Interface Specification Language for Java. ACM SIGSOFT Software Engineering Notes, 31(3):1-38, March 2006.
`http://doi.acm.org/10.1145/1127878.1127884'. Also Iowa State University, Department of Computer Science, TR #98-06-rev29, January 2006, which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.pdf'.

[Leavens-Cheon06]

Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML. December, 2006, which is available from the URL
`http://www.jmlspecs.org/jmldbc.pdf'.

[Leavens-Dhara00]

Gary T. Leavens and Krishna Kishore Dhara. Concepts of Behavioral Subtyping and a Sketch of Their Extension to Component-Based Systems. In Gary T. Leavens and Murali Sitaraman (eds.), Foundations of Component-Based Systems, Cambridge University Press, 2000, pp. 113-135.
`http://www.eecs.ucf.edu/~leavens/FoCBS-book/06-leavens-dhara.pdf'

[Leavens-etal05]

G. T. Leavens, Y. Cheon, C. Clifton, C. Ruby, and D. R. Cok. How the design of JML accommodates both runtime assertion checking and formal verification Science of Computer Programming, 55(1-3):185-208, 2005.

[Leavens-Mueller07]

Gary T. Leavens and Peter Müller. Information Hiding and Visibility in Interface Specifications. In International Conference on Software Engineering (ICSE), pages 385-395, IEEE, 2007. `http://dx.doi.org/10.1109/ICSE.2007.44'

[Leavens-Naumann06]

Gary T. Leavens and David A. Naumann. Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. Department of Computer Science, TR \#06-20b, July 2006, revised August, September 2006. Available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR90-09/TR.pdf'.

[Leavens-Weihl90]

Gary T. Leavens and William E. Weihl. Reasoning about Object-oriented Programs that use Subtypes (extended abstract). In N. Meyrowitz (ed.), OOPSLA ECOOP '90 Proceedings (ACM SIGPLAN Notices, 25(10):212-223, October 1990).

[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-Wing98]

Gary T. Leavens and Jeannette M. Wing. Protective interface specifications. Formal Aspects of Computing, 10(1):590-75, January 1998.

[Leavens90]

Gary T. Leavens. Modular Verification of Object-Oriented Programs with Subtypes. Department of Computer Science, Iowa State University (Ames, Iowa, 50011), TR 90-09, July 1990. Available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR90-09/TR.ps.Z'.

[Leavens91]

Gary T. Leavens. Modular Specification and Verification of Object-Oriented Programs. IEEE Software, 8(4):72-80, July 1991.

[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 (Kluwer Academic Publishers, 1996), Chapter 8, pages 121-142. An extended version is Department of Computer Science, Iowa State University, TR #96-01c, July 1996, which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR96-01/TR.ps.Z'.

[Leavens97c]

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

[Leavens06b]

Gary T. Leavens. JML's Rich, Inherited Specifications for Behavioral Subtypes. In Zhiming Liu and He Jifeng (eds), Proceedings, International Conference on Formal Engineering Methods (ICFEM'06), Macao, China, pages 2-36. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006. Also Department of Computer Science, Iowa State University, TR \#06-22, August 2006.
`ftp://ftp.cs.iastate.edu/pub/techreports/TR06-22/TR.pdf'

[Ledgard80]

Henry. F. Ledgard. A Human Engineered Variant of BNF. ACM SIGPLAN Notices, 15(10):57-62, October 1980.

[Leino-Nelson-Saxe00]

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

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

[Leino95]

K. Rustan M. Leino. Towards Reliable Modular Programs. PhD thesis, California Institute of Technology, January 1995. Available from the URL
`ftp://ftp.cs.caltech.edu/tr/cs-tr-95-03.ps.Z'.

[Leino95b]

K. Rustan M. Leino. A myth in the modular specification of programs. KRML 63, November 1995. Obtained from the author (rustan@pa.dec.com).

[Leino98]

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

[Lerner91]

Richard Allen Lerner. Specifying Objects of Concurrent Systems. School of Computer Science, Carnegie Mellon University, CMU-CS-91-131, May 1991. Available from the URL
`ftp://ftp.cs.cmu.edu/afs/cs.cmu.edu/project/larch/ftp/thesis.ps.Z'.

[Liskov-Guttag86]

Barbara Liskov and John Guttag. Abstraction and Specification in Program Development (MIT Press, Cambridge, Mass., 1986).

[Liskov-Wing93b]

Barbara Liskov and Jeannette M. Wing. Specifications and their use in defining subtypes. In Andreas Paepcke, editor, OOPSLA '93 Proceedings. (ACM SIGPLAN Notices 28(10):16-28, October, 1993.)

[Liskov-Wing94]

Barbara Liskov and Jeannette M. Wing. A Behavioral Notion of Subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811-1841, November 1994.

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

[Morgan-Vickers94]

Carroll Morgan and Trevor Vickers. On the refinement calculus. Springer-Verlag, New York, N.Y., 1994.

[Morgan94]

Carroll Morgan. Programming from Specifications, second edition (Prentice-Hall, 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.

[Mueller-Poetzsch-Heffter00]

Peter Müller and Arnd Poetzsch-Heffter. Modular Specification and Verification Techniques for Object-Oriented Software Components. In Gary T. Leavens and Murali Sitaraman (eds.), Foundations of Component-Based Systems, pages 137-159. Cambridge University Press, 2000.

[Mueller-Poetzsch-Heffter00a]

Peter Müller and Arnd Poetzsch-Heffter. A Type System for Controlling Representation Exposure in Java. In S. Drossopoulou, et al. (eds.), Formal Techniques for Java Programs, 2000. Technical Report 269, Fernuniversität Hagen, Available from
`http://www.informatik.fernuni-hagen.de/pi5/publications.html'

[Mueller-Poetzsch-Heffter01a]

Peter Müller and Arnd Poetzsch-Heffter. Universes: A Type System for Alias and Dependency Control. Technical Report 279, Fernuniversität Hagen, 2001. Available from
`http://www.informatik.fernuni-hagen.de/pi5/publications.html'

[Mueller-Poetzsch-Heffter-Leavens03]

Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. Concurrency and Computation: Practice and Experience, 15(2):117-154, February 2003. Also Technical Report TR #02-02, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, February 2002. Available from
`ftp://ftp.cs.iastate.edu/pub/techreports/TR02-02/TR.pdf'

[Mueller-Poetzsch-Heffter-Leavens06]

Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Invariants for Layered Object Structures. Science of Computer Programming, 62(3):253-286, October 2006.
`http://dx.doi.org/10.1016/j.scico.2006.03.001' Also Technical Report 424, ETH Zürich, October 2003, revised March 2004, March 2005. Available from
`ftp://ftp.inf.ethz.ch/pub/publications/tech-reports/4xx/424.pdf'

[Mueller02]

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

[Nelson89]

Greg Nelson. A Generalization of Dijkstra's Calculus. ACM Transactions on Programming Languages and Systems, 11(4):517-561, October 1989.

[Noble-Vitek-Potter98]

James Noble, Jan Vitek, and John Potter. Flexible Alias Protection. In Eric Jul (ed.), ECOOP '98 -- Object-Oriented Programming, 12th European Conference, Brussels, Belgium, pages volume 1445 of Lecture Notes in Computer Science, pages 158-185. Springer-Verlag, New York, N.Y., 1998.

[Parnas72]

D. L. Parnas. On the Criteria to be Used in Decomposing Systems into Modules. Comm. ACM, 15(12):1053-1058, December 1972.

[Poetzsch-Heffter97]

Arnd Poetzsch-Heffter. Specification and Verification of Object-Oriented Programs. Habilitationsschrift, Technische Universitaet Muenchen, 1997. Available from the URL
`http://wwweickel.informatik.tu-muenchen.de/persons/poetzsch/habil.ps.gz'.

[Jacobs-Poll01]

Bart Jacobs and Eric Poll. A Logic for the Java Modeling Language JML. In Fundamental Approaches to Software Engineering (FASE'2001), Genova, Italy, 2001. Volume 2029 of Lecture Notes in Computer Science, Springer-Verlag, 2001. `http://www.cs.kun.nl/~erikpoll/publications/jmllogic.html'

[Raghavan-Leavens05]

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

[Rioux-Chalin07]

F. Rioux and P. Chalin. Effective and Efficient Runtime Assertion Checking for JML Through Strong Validity. Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs (FTfJP'07), Berlin, Germany, 2007.

[Rodriguez-etal05]

Edwin Rodriguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby. Extending JML for Modular Specification and Verification of Multi-Threaded Programs. In Andrew P. Black (ed.), ECOOP 2005 -- Object-Oriented Programming 19th European Conference, Glasgow, UK, pages 551-576. Volume 3586 of Lecture Notes in Computer Science, Springer Verlag, July 2005.

[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. (ACM SIGPLAN Notices, 35(10):208-228, 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'.

[Ruby06]

Clyde Dwain Ruby. Modular subclass verification: safely creating correct subclasses without superclass code. Ph.D. Thesis, Department of Computer Science, Iowa State University. Also Technical Report #06-34, December 2006. Available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR06-34/TR.pdf'.

[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'

[Shaner-Leavens-Naumann07]

Steve M. Shaner, Gary T. Leavens, and David A. Naumann. Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model Programs Department of Computer Science, Iowa State University, TR #07-04a, March 2007, revised April 2007, which is available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR07-04/TR.pdf'.

[Spivey92]

J. Michael Spivey. The Z Notation: A Reference Manual, second edition, (Prentice-Hall, Englewood Cliffs, N.J., 1992).

[Steyaert-etal96]

Patrick Steyaert, Carine Lucas, Kim Mens, and Theo D'Hondt. Issues in the Design and Documentation of Class Libraries. In OOPSLA '96 Proceedings. (ACM SIGPLAN Notices, 31(10):268-285, October, 1996.)

[Tan95]

Yang Meng Tan. Formal Specification Techniques for Engineering Modular C Programs. International Series in Software Engineering (Kluwer Academic Publishers, Boston, 1995). Also published as Formal Specification Techniques for Promoting Software Modularity, Enhancing Documentation, and Testing Specifications. Technical Report TR-619, MIT Lab. for Comp. Sci., June 1994.

[Watt91]

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

[Wills92b]

Alan Wills. Specification in Fresco. In Susan Stepney and Rosalind Barden and David Cooper (eds.), Object Orientation in Z, chapter 11, pages 127-135. Springer-Verlag, Workshops in Computing Series, Cambridge CB2 1LQ, UK, 1992.

[Wing83]

Jeannette Marie Wing. A Two-Tiered Approach to Specifying Programs Technical Report TR-299, Mass. Institute of Technology, Laboratory for Computer Science, 1983.

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