|
|
| Home > FAQ on different themes > |
Larch Frequently Asked Questions (comp.specification.larch FAQ) |
Section 7 of 7 - Prev - Next
All sections - 1 - 2 - 3 - 4 - 5 - 6 - 7
Formal Software Development Methods 4th International Symposium of VDM
Europe Noordwijkerhout, The Netherlands, Volume 2: Tutorials. Lecture
Notes in Computer Science, vol. 552, (Springer-Verlag, NY, 1991), pages
1-78.
[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. Texts and Monographs in Computer Science series
(Springer-Verlag, NY, 1993). (The ISBN numbers are 0-387-94006-5 and
3-540-94006-5.) This is currently out of print, but a (large)
postscript file for the entire book can be obtained from the following
URL
`http://www.sds.lcs.mit.edu/spd/larch/pub/larchBook.ps'.
Appendix A is available separately from the following URLs.
`http://www.research.digital.com/SRC/larch/toc.html'
`http://www.research.digital.com/SRC/larch/handbook.ps'
[Guttag75]
John V. Guttag. The Specification and Application to Programming of
Abstract Data Types. Ph.D. Thesis, University of Toronto, Toronto,
Canada, September, 1975.
[Hall90]
Anthony Hall. Seven Myths of Formal Methods. IEEE Software, 7(5):11-19
(Sept. 1990).
[Hayes93]
I. Hayes (ed.), Specification Case Studies, second edition
(Prentice-Hall, Englewood Cliffs, N.J., 1990).
[Hoare69]
C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Comm. ACM,
12(10):576-583 (Oct. 1969).
[Hoare72a]
C. A. R. Hoare. Proof of correctness of data representations. Acta
Informatica, 1(4):271-281 (1972).
[ISO-VDM96]
International Standards Organization. Information technology --
Programming languages, their environments and system software
interfaces -- Vienna Development Method -- Specification Language --
Part 1: Base language. Document ISO/IEC 13817-1, December, 1996.
[Jackson95]
Daniel Jackson. Structuring Z Specifications with Views. ACM
Transactions on Software Engineering and Methodology, 4(4):365-389
(Oct, 1995).
[Jones90]
Cliff B. Jones, Systematic software development using VDM, second
edition (Prentice-Hall, Englewood Cliffs, N.J., 1990). Out-of-print,
but available on-line at the URL
`http://www.cs.ncl.ac.uk/people/cliff.jones/home.formal/research-other.html'
[Jones91]
Kevin D. Jones. LM3: A Larch Interface Language for Modula-3: A
Definition and Introduction: Version 1.0. Technical Report 72, Digital
Equipment Corp, Systems Research Center, 130 Lytton Avenue Palo Alto,
CA 94301, June, 1991. Order from src-report@src.dec.com or from the URL
`http://www.research.digital.com/SRC/publications/src-rr.html'.
[Jones93]
Kevin D. Jones. A Semantics for a Larch/Modula-3 Interface Language. In
[Martin-Wing93], pages 142-158.
[Jonkers91]
H. B. M. Jonkers. Upgrading the pre- and postcondition technique. In S.
Prehn and W. J. Toetenel (eds.), 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, NY, 1991.
[Kaufmann-Moore97]
Matt Kaufmann and J S. Moore. An Industrial Strength Theorem Prover for
a Logic Based on Common Lisp. IEEE Transactions on Software
Engineering, 23(4):203-213 (Apr. 1997).
[Khosla-Maibaum87]
S. Khosla and T. S. E. Maibaum. The Prescription and Description of
State Based Systems. In B. Banieqbal, H. Barringer, and A. Puneli
(eds.), Temporal Logic in Specification. Volume 398 of Lecture Notes in
Computer Science, pages 243-294. Springer-Verlag, NY, 1987.
[Lamport89]
Leslie Lamport. A Simple Approach to Specifying Concurrent Systems.
CACM, 32(1):32-45 (Jan. 1989).
[Leavens97]
Gary T. Leavens. Larch/C++ Reference Manual. Version 5.14, October
1997. Available in `ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz'
or on the world wide web via the URL
`http://www.cs.iastate.edu/~leavens/larchc++.html'.
[Leavens96b]
Gary T. Leavens. An Overview of Larch/C++: Behavioral Specifications
for C++ Modules. Technical Report TR #96-01d, Department of Computer
Science, Iowa State University, Ames, Iowa, 50011, April 1996, revised
July 1997. 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. TR version
available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR96-01/TR.ps.gz'.
[Leavens-Wing97]
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, pages 520-534. An extended version
is Technical Report TR #96-04d, Department of Computer Science, Iowa
State University, Ames, Iowa, 50011, April 1996, revised October,
December 1996, February, September 1997. Available from the URL
`ftp://ftp.cs.iastate.edu/pub/techreports/TR96-04/TR.ps.gz'.
[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).
[Loeckx-Ehrich-Wolf96]
Jacques Loeckx, Hans-Dieter Ehrich, and Markus Wolf Specification of
Abstract Data Types (John Wiley & Sons Ltd and B. G. Teubner, NY,
1996).
[Luchangco-etal94]
Victor Luchangco, Ekrem Soylemez, Stephen Garland, and Nancy Lynch.
Verifying timing properties of concurrent algorithms. In FORTE'94:
Seventh International Conference on Formal Description Techniques for
Distributed Systems and Communications Protocols, Berne, Switzerland
(Chapman and Hall, Oct. 1994).
[Martin-Lai92]
U. Martin and M. Lai. Some experiments with a completion theorem
prover. Journal of Symbolic Computation, 13:81-100 (1992).
[Martin-Wing93]
U. Martin and J. Wing. Proceedings of the First International Workshop
on Larch, July 1992. Workshops in Computing series (Springer-Verlag,
New York, 1993). (The ISBN is 0-387-19804-0.)
[Meyer92]
Bertrand Meyer. Applying "Design by Contract". Computer, 25(10):40-51
(Oct. 1992).
[Meyer97]
Bertrand Meyer. Object-oriented Software Construction, second edition
(Prentice-Hall, 1997).
[Mosses96]
Peter D. Mosses (editor). CFI Catalogue: Language Design. May 1996.
Available from the URL
`http://www.brics.dk/Projects/CFI/Catalogue/2/index.html'.
[ORA94]
Odyssey Research Associates. Penelope Reference Manual, Version 3-3.
Informal Technical Report STARS-AC-C001/001/00, September 1994.
Available from the URL
`http://source.asset.com/WSRD/ASSET/A/874/elements/RefManual.tty'.
[Owre-etal95]
Formal Verification for Fault-tolerant Architectures: Prolegomena to
the Deisgn of PVS. Sam Owre, John Rushby, Natarajan Shankar, and
Friedrich von Henke. IEEE Transactions on Software Engineering,
21(2):107-125 (February 1995). See also the URL
`http://www.csl.sri.com/pvs.html'.
[Paulson94]
Lawrence C. Paulson, with contributions by Tobias Nipkow. Isabelle: A
Generic Theorem Prover. Volume 828 of Lecture Notes in Computer
Science, Springer-Verlag 1994. See also the URL
`http://www.cl.cam.ac.uk/Research/HVG/isabelle.html'.
[Saiedian-etal96]
An Invitation to Formal Methods. Hossein Saiedian, et al. IEEE
Computer, 29(4):16-30 (April 1996).
[Saxe-etal92]
J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning. Using
transformations and verification in circuit design. International
Workshop on Designing Correct Circuits, IFIP Transactions A-5,
(North-Holland 1992). Also Technical Report 78, Digital Equipment Corp,
Systems Research Center, 130 Lytton Avenue Palo Alto, CA 94301,
September 1991.
[Schmidt86]
David A. Schmidt. Denotational Semantics: A Methodology for Language
Development (Allyn and Bacon, Inc., Boston, Mass., 1986).
[Sitaraman-Welch-Harms93]
M. Sitaraman, L. R. Welch, and D. E. Harms. On Specification of
Reusable Software Components. International Journal of Software
Engineering and Knowledege Engineering, 3(2):207-229 (World Scientific
Publishing Company, 1993).
[Sivaprasad95]
Gowri Sankar Sivaprasad. Larch/CORBA: Specifying the Behavior of
CORBA-IDL Interfaces. Department of Computer Science, Iowa State
University, TR #95-27a, December 1995, revised December 1995.
[Soegaard-Anderson-etal93]
J. F. Soegaard-Anderson, S. J. Garland, J. V. Guttag, N. A. Lynch, and
A. Pogosyants. Computed-assisted simulation proofs. In Fourth
Conference on Computer-Aided Verification, Elounda, Greece, Volume 697
of Lecture Notes in Computer Science, pages 305-319 (Springer-Verlag,
June 1993).
[Spivey92]
J. Michael Spivey. The Z Notation: A Reference Manual, second edition,
(Prentice-Hall, Englewood Cliffs, N.J., 1992).
[Staunstrup-Garland-Guttag89]
J. Staunstrup, S. J. Garland, and J. V. Guttag. Localized verification
of circuit descriptions. In Proc. Int. Workshop on Automatic
Verification Methods for Finite State Systems, Grenoble, France. Volume
407 of Lecture Notes in Computer Science, pages 349-364
(Springer-Verlag, 1989).
[Staunstrup-Garland-Guttag92]
J. Staunstrup, S. J. Garland, and J. V. Guttag. Mechanized verification
of circuit descriptions using the Larch Prover. In Theorem Provers in
Circuit Design. IFIP Transactions A-10, pages 277-299 (North-Holland,
June, 1992).
[Tan94]
Yang Meng Tan. Formal Specification Techniques for Promoting Software
Modularity, Enhancing Documentation, and Testing Specifications. MIT
Lab. for Comp. Sci., TR 619, June 1994. Also published as Formal
Specification Techniques for Engineering Modular C Programs.
International Series in Software Engineering (Kluwer Academic
Publishers, Boston, 1995).
[Wing-Rollins-Zaremski93]
Jeannette M. Wing, Eugene Rollins, and Amy Moormann Zaremski. Thoughts
on a Larch/ML and a New Application for LP. In [Martin-Wing93], pages
297-312.
[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 (Jan.
1987).
[Wing90]
Jeannette M. Wing. A Specifier's Introduction to Formal Methods.
Computer, 23(9):8-24 (Sept. 1990)
[Wing95]
Jeannette M. Wing. Hints to Specifiers. Technical Report,
CMU-CS-95-118R, Carnegie Mellon University, School of Computer Science,
May 1995. Revision of the paper, "Teaching Mathematics to Software
Engineers," Proceedings of AMAST '95, July 1995. Revision available
from the URL
`http://www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/papers/education/paper.ps'.
--
Department of Computer Science, Iowa State University
229 Atanasoff Hall, Ames, Iowa 50011-1040 USA
leavens@cs.iastate.edu phone: +1 515 294-1580 fax: +1 515 294-0258
URL: http://www.cs.iastate.edu/~leavens
Section 7 of 7 - Prev - Next
All sections - 1 - 2 - 3 - 4 - 5 - 6 - 7
| Back to category FAQ on different themes - Use Smart Search |
| Home - Smart Search - About the project - Feedback |
© allanswers.org | Terms of use