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.