Bibliography

1

A. J. Alencar and J. A. Goguen.
OOZE: An object oriented Z environment.
In P. America, editor, ECOOP '91: European Conference on Object Oriented Programming, volume 512 of Lecture Notes in Computer Science, pages 180-199. Springer-Verlag, New York, N.Y., 1991.

2

A. J. Alencar and J. A. Goguen.
OOZE.
In Stepney et al. [45], pages 79-94.

3

A. J. Alencar and J. A. Goguen.
Specification in OOZE with examples.
In Lano and Haughton [23], pages 158-183.

4

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, N.Y., June 1987. Springer-Verlag.
Lecture Notes in Computer Science, Volume 276.

5

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, N.Y., 1991.

6

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

7

Patrice Chalin.
On the Language Design and Semantic Foundation of LCL, a Larch/C Interface Specification Language.
PhD thesis, Concordia University, 1455 de Maisonneuve Blvd. West, Montreal, Quebec, Canada, October 1995.
Available as CU/DCS TR 95-12, from the URL ftp://ftp.cs.concordia.ca/pub/chalin/tr.ps.Z.

8

Patrice Chalin, Peter Grogono, and T. Radhakrishnan.
Identification of and solutions to shortcomings of LCL, a Larch/C interface specification language.
In Marie-Claude Gaudel and James Woodcock, editors, FME '96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 385-404, New York, N.Y., March 1996. Springer-Verlag.

9

Yoonsik Cheon and Gary T. Leavens.
The Larch/Smalltalk interface specification language.
ACM Transactions on Software Engineering and Methodology, 3(3):221-253, July 1994.

10

Elspeth Cusack and G. H. B. Rafsanjani.
ZEST.
In Stepney et al. [45], pages 113-126.

11

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.

12

Margaret A. Ellis and Bjarne Stroustrup.
The Annotated C++ Reference Manual.
Addison-Wesley Publishing Co., Reading, Mass., 1990.

13

Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, and Jose Meseguer.
Principles of OBJ2.
In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 52-66. ACM, January 1985.

14

Joseph A. Goguen.
Parameterized programming.
IEEE Transactions on Software Engineering, SE-10(5):528-543, September 1984.

15

David Guaspari, Carla Marceau, and Wolfgang Polak.
Formal verification of Ada programs.
IEEE Transactions on Software Engineering, 16(9):1058-1075, September 1990.

16

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.

17

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

18

Wim H. Hesselink.
Programs, Recursion, and Unbounded Choice, volume 27 of Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, New York, N.Y., 1992.

19

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

20

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

21

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

22

Leslie Lamport.
A simple approach to specifying concurrent systems.
Communications of the ACM, 32(1):32-45, January 1989.

23

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

24

K. Lano and H. Haughton.
Specifying a concept-recognition system in Z++.
In Lano and Haughton [23], chapter 7, pages 137-157.

25

Kevin C. Lano.
Z++.
In Stepney et al. [45], pages 106-112.

26

Gary T. Leavens.
Modular specification and verification of object-oriented programs.
IEEE Software, 8(4):72-80, July 1991.

27

Gary T. Leavens.
Inheritance of interface specifications (extended abstract).
In Proceedings of the Workshop on Interface Definition Languages, volume 29(8) of ACM SIGPLAN Notices, pages 129-138, August 1994.

28

Gary T. Leavens.
LSL math traits.
http://www.cs.iastate.edu/~leavens/Math-traits.html, Jan 1996.

29

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.

30

Gary T. Leavens.
Larch/C++ Reference Manual.
Version 5.25. Available in ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz or on the World Wide Web at the URL http://www.cs.iastate.edu/~leavens/larchc++.html, January 1999.

31

Gary T. Leavens and William E. Weihl.
Reasoning about object-oriented programs that use subtypes (extended abstract).
In N. Meyrowitz, editor, OOPSLA ECOOP '90 Proceedings, volume 25(10) of ACM SIGPLAN Notices, pages 212-223. ACM, October 1990.

32

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.

33

Gary T. Leavens and Jeannette M. Wing.
Protective interface specifications.
Technical Report 96-04d, Iowa State University, Department of Computer Science, September 1997.
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, Springer-Verlag, 1997, pages 520-534. Available by anonymous ftp from ftp.cs.iastate.edu or by e-mail from almanac@cs.iastate.edu.

34

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

35

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

36

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

37

Silvio Lemos Meira and Ana Lúcia C. Cavalcanti.
MooZ case studies.
In Stepney et al. [45], pages 37-58.

38

Silvio Lemos Meira, Ana Lúcia C. Cavalcanti, and Cassio Souza Santos.
The Unix filing system: A MooZ specification.
In Lano and Haughton [23], chapter 4, pages 80-109.

39

Swapan Mitra.
Object-oriented specification in VDM++.
In Lano and Haughton [23], chapter 6, pages 130-136.

40

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

41

Gordon Rose.
Object-Z.
In Stepney et al. [45], pages 59-77.

42

Gordon Rose and Roger Duke.
An Object-Z specification of a mobile phone system.
In Lano and Haughton [23], chapter 5, pages 110-129.

43

J. Spivey.
An introduction to Z and formal specifications.
Software Engineering Journal, January 1989.

44

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

45

Susan Stepney, Rosalind Barden, and David Cooper, editors.
Object Orientation in Z.
Workshops in Computing. Springer-Verlag, Cambridge CB2 1LQ, UK, 1992.

46

Bjarne Stroustrup.
The C++ Programming Language: Second Edition.
Addison-Wesley Publishing Co., Reading, Mass., 1991.

47

Yang Meng Tan.
Formal specification techniques for promoting software modularity, enhancing documentation, and testing specifications.
Technical Report 619, Massachusetts Institute of Technology, Laboratory for Computer Science, 545 Technology Square, Cambridge, Mass., June 1994.

48

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.

49

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.

50

Alan Wills.
Capsules and types in Fresco: Program validation in Smalltalk.
In P. America, editor, ECOOP '91: European Conference on Object Oriented Programming, volume 512 of Lecture Notes in Computer Science, pages 59-76. Springer-Verlag, New York, N.Y., 1991.

51

Alan Wills.
Specification in Fresco.
In Stepney et al. [45], chapter 11, pages 127-135.

52

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

53

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

54

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