Larch/C++ Reference Manual
|
Home About Browse Search Register Subscriptions Deposit Papers Help |
Leavens, Gary T. (1999) Larch/C++ Reference Manual.
| Full text available as: | Postscript Adobe PDF HTML |
Abstract
Larch/C++ is a notation for formally specifying the behavior and interfaces of C++ classes and functions. The goal of this reference manual is to precisely record the design of Larch/C++. We try to give examples and explanations, and we hope that these will be helpful to readers trying to learn about formal specification using Larch/C++.
| Keywords: | Specification, verification, Larch, C++, behavioral interface specification language, redundancy, examples, refinement, frame axioms, pre- and postconditions |
| Comments: | The Larch/C++ web page is http://www.cs.iastate.edu/~leavens/larchc++.html |
| Subjects: | Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1) Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1) Software: SOFTWARE ENGINEERING (K.6.3): Distribution, Maintenance, and Enhancement Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1) |
| ID code: | 00000243 |
| Deposited by: | Gary T. Leavens on 03 August 2001 |
| Alternative Locations: | ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.ps.gz ftp://ftp.cs.iastate.edu/pub/larchc++/lcpp.dvi.gz |
Contact site administrator at: ssg@cs.iastate.edu