next up previous
Next: Satisfaction Up: Larch/C++ An Interface Specification Previous: Larch/C++ An Interface Specification

What is Larch/C++?

Larch/C++ is a behavioral interface specification language. In such a language once does both:

The idea of behavioral specification is to describe ``what, not how.'' One specifies what a module does, not how it does it.

As an analogy consider coke (vending) machine:

So this is not just math, the interface is a physical thing. (See Lamport's paper ``A Simple Approach to Specifying Concurrent Systems'' CACM, January 1989.)

Q: Is Larch/C++ designed to specify the behavior of an entire C++ program?

A: No, because it designed to specify parts of C++ programs, called from other parts.

The picture in Figure 1 illustrates this idea.

Figure 1: The idea of behavioral interface specification in Larch/C++.
\begin{figure}\vspace{-2ex} \begin{flushleft}\rule{\textwidth}{0.01in}\end{flush...{flushleft}\rule{\textwidth}{0.01in}\end{flushleft} \vspace{-2ex}

Gary T. Leavens