\begin{thebibliography}{10}

\bibitem{Beck-Gamma98}
Kent Beck and Erich Gamma.
\newblock Test infected: Programmers love writing tests.
\newblock {\em Java Report}, 3(7):37--50, 1998.

\bibitem{Burdy-etal05}
Lilian Burdy, Yoonsik Cheon, David~R. Cok, Michael~D. Ernst, Joeseph~R. Kiniry,
  Gary~T. Leavens, K.~Rustan~M. Leino, and Erik Poll.
\newblock An overview of {JML} tools and applications.
\newblock {\em International Journal on Software Tools for Technology Transfer
  (STTT)}, 7(3):212--232, June 2005.

\bibitem{Cheon03}
Yoonsik Cheon.
\newblock A runtime assertion checker for the {Java Modeling Language}.
\newblock Technical Report 03-09, Department of Computer Science, Iowa State
  University, Ames, IA, April 2003.
\newblock The author's Ph.D. dissertation. Available from
  \url{archives.cs.iastate.edu}.

\bibitem{Cheon-Leavens02b}
Yoonsik Cheon and Gary~T. Leavens.
\newblock A runtime assertion checker for the {Java Modeling Language (JML)}.
\newblock In Hamid~R. Arabnia and Youngsong Mun, editors, {\em Proceedings of
  the International Conference on Software Engineering Research and Practice
  (SERP '02), Las Vegas, Nevada, USA, June 24-27, 2002}, pages 322--328. CSREA
  Press, June 2002.

\bibitem{Cheon-Leavens02}
Yoonsik Cheon and Gary~T. Leavens.
\newblock A simple and practical approach to unit testing: The {JML} and
  {JUnit} way.
\newblock In Boris Magnusson, editor, {\em ECOOP 2002 --- Object-Oriented
  Programming, 16th European Conference, M\'{a}alaga, Spain, Proceedings},
  volume 2374 of {\em Lecture Notes in Computer Science}, pages 231--255,
  Berlin, June 2002. Springer-Verlag.

\bibitem{Cheon-etal05}
Yoonsik Cheon, Gary~T. Leavens, Murali Sitaraman, and Stephen Edwards.
\newblock Model variables: Cleanly supporting abstraction in design by
  contract.
\newblock {\em Software: Practice and Experience}, 35(6):583--599, May 2005.

\bibitem{Hoare69}
C.~A.~R. Hoare.
\newblock An axiomatic basis for computer programming.
\newblock {\em Communications of the ACM}, 12(10):576--583, October 1969.

\bibitem{Leavens-Baker-Ruby06}
Gary~T. Leavens, Albert~L. Baker, and Clyde Ruby.
\newblock Preliminary design of {JML}: A behavioral interface specification
  language for {Java}.
\newblock {\em ACM SIGSOFT Software Engineering Notes}, 31(3):1--38, March
  2006.
\newblock \url{http://doi.acm.org/10.1145/1127878.1127884}.

\bibitem{Leavens-etal05}
Gary~T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David~R. Cok.
\newblock How the design of {JML} accommodates both runtime assertion checking
  and formal verification.
\newblock {\em Science of Computer Programming}, 55(1-3):185--208, March 2005.

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

\bibitem{Meyer92a}
Bertrand Meyer.
\newblock Applying ``design by contract''.
\newblock {\em Computer}, 25(10):40--51, October 1992.

\bibitem{Meyer92b}
Bertrand Meyer.
\newblock {\em Eiffel: The Language}.
\newblock Object-Oriented Series. Prentice Hall, New York, NY, 1992.

\end{thebibliography}
