Definition

In FreeSpec, a component is an entity which exposes an interface i, and uses primitives of an interface j to compute the results of primitives of i. Besides, a component is likely to carry its own internal state (of type s).

                           i +-------------------+      j
                           | |                   |      |
                   +------>| | c : component i j |----->|
                           | |                   |      |
                             +-------------------+

Thus, a component c : component i j is a polymorphic function which maps primitives of i to impure computations using j.

The similarity between FreeSpec components and operational semantics may be confusing at first. The main difference between the two concepts is simple: operational semantics are self-contained terms which can, alone, be used to interpret impure computations of a given interface. Components, on the other hand, are not self-contained. Without an operational semantics for j, we cannot use a component c : component i j to interpret an impure computation using i. Given an initial semantics for j, we can however derive an operational semantics for i from a component c.

Semantics Derivation

So, semprod on the one hand allows for composing operational semantics horizontally, and derive_semantics allows for composing components vertically. Using these two operators, we can model a complete system in a hierarchical and modular manner, by defining each of its components independently, then composing them together with semprod and derive_semantics.

In-place Primitives Handling

The function with_component allows for locally providing an additional interface j within an impure computation of type impure ix a. The primitives of j will be handled by impure computations, i.e., a component. of type c : compoment j ix s.