archives

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