What is Larch/C++?

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

• behavioral specification, which describes what a program module does, and

• interface specification, which describes how C++ clients see the module.

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:

• behavior is 55 cents gives a coke,
• interface is buttons you push.

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++.