Languages

The distinction between a language and its underlying model of computation is important. The same model of computation can give rise to fairly different languages (e.g., the imperative Algol-like languages C, C++, Pascal, and FORTRAN). Some languages, such as VHDL and Verilog, support two or more models of computation7.
The model of computation affects the expressiveness of a language — which behaviors can be described in the language, whereas the syntax affects compactness, modularity, and reusability. Thus, for example, object-oriented properties of imperative languages like C++ are more a matter of syntax than a model of computation. The expressiveness of a language is an important issue. At one extreme, a language that is not expressive enough to specify a particular behavior is clearly unsuitable, but the other extreme also raises problems. A language that is too expressive often raises the complexity of analysis and synthesis. In fact, for very expressive languages, many analysis and synthesis problems become undecidable: no algorithmwill solve all problem instances in finite time. A language in which a desired behavior cannot be represented succinctly is also problematic. The difficulty of solving analysis and synthesis problems is at least linear in the size of the problem description, and can be as bad as several times exponential, so choosing a language in which the desired behavior of the system is compact can be critical. A language may be very incomplete and/or very abstract. For example, it may specify only the interaction between computational modules, and not the computation performed by the modules. Instead, it provides an interface to a host language that specifies the computation, and is called a coordination language (examples include Linda [41], Granular Lucid [39], and Ptolemy domains [14]). Or the language may specify only the causality constraints of the interactions without detailing the interactions themselves nor providing an interface to a host language. In this case, the language is used as a tool to prove properties of systems, as done, for example, in process calculi [46], [47] and Petri nets [48], [49]. In still more abstract modeling, components in the system are replaced with nondeterminate specifica- 7They directly support the Imperative model within a process, and the Discrete Event model among processes. They can also support Extended Finite State Machines under suitable restrictions known as the “synthesizable subset”. tions that give constraints on the behavior, but not the behavior itself. Such abstraction provides useful simplifications that help formal verification.
C. Languages