Getting Started¶

A Calculator program in Erlang¶

Let us consider an archetypal calculator program consisting of a single server process that handles client requests for arithmetic computation. The calculator server blocks and waits for requests sent as asynchronous messages. These messages are addressed to the server using its PID, and deposited in the server mailbox that buffers multiple client requests. The calculator server unblocks upon reading a message from its mailbox. In our client-server protocol, messages contain the type of operation to be executed on the server side, its arguments (if applicable), and the client PID to whom the corresponding server reply is addressed.

Our calculator program is implemented as the Erlang module calc_server that can be found under examples/erlang/src.

start(N) ->
  spawn(?MODULE, loop, [N]).

loop(Tot) ->
  receive
    {Clt, {add, A, B}} ->
      Clt ! {ok, A + B},
      loop(Tot + 1);

    {Clt, {mul, A, B}} ->
      Clt ! {ok, A * B},
      loop(Tot + 1);

    {Clt, stp} -> % Stop service.
      Clt ! {bye, Tot}
  end.

calc_server:loop/1 encapsulates the calculator server logic that is spawned by some other launcher process (e.g. the Erlang shell) that invokes calc_server:start/1 for some integer argument N.

The spawned server consumes a message request from its mailbox via the receive expression on lines 5-16, and pattern matches against one of the three types of operations requested by clients:

Addition (add) and multiplication (mul) requests that carry the operands A and B (lines 6 and 10), and,
stop (stp) requests that carries no arguments (line 14).

Pattern matching instantiates the variables Clt, A and B to concrete data in client request messages. Every request fulfilled by the server results in a corresponding reply that it sends to the PID of the client instantiated in variable Clt, lines 6, 10, and 14. Server replies carry the status tag (an atom) ok or bye, and the result of the requested operation. The server uses the parameter Tot of loop/1 to track the number of requests serviced, and is returned in reply to a stp operation. After handling add and mul requests, the server executes loop/1 to recommence the process loop and service the next client request, incrementing the request count accordingly (lines 8 and 12); the tail recursive call to loop/1 is not made for stp requests, and the calculator server process terminates naturally.

The logic of loop/1 induces a server runtime behaviour that can be abstractly described by the transition system model below.

States of the model capture the internal state that the server process can be in at any point during its execution. Transitions between states denote the computational steps of the program that produce visible program events. For instance, the event Srv ? {Clt, stp} is exhibited by the server loop when the calculator at its initial state Q0 reads a stp request from its mailbox and transitions to Q3. This transition depicts the computation that loop/1 performs to receive the stp request, line 5, and subsequently pattern match it to {Clt, stp} on line 14. Note that events in the model capture the set of all possible concrete events that the running program can exhibit, e.g., Srv ? {Clt, stp} describes all receive events where the variable placeholders Srv and Clt range over PIDs, and stp is the atom denoting the stop operation requested by clients.

Safety properties¶

There are a number of properties we would like the server behaviour to observe. For example, the server loop does not control the initial value of Tot that an invocation to calc_server:start/1 provides. We could, therefore, require that:

(P₁) The service request count returned on shutdown is never negative.

Similarly, we would expect that

(P₂) Replies are always sent to the client indicated in the request,

and that

(P₃) A request for adding two numbers always returns their sum

both hold, amongst others.

These properties are data-dependent, which makes them hard to ascertain using static techniques such as type systems. Besides properties that reason about data, our server logic is expected to comply with control properties, such as,

(P₄) Client requests are never serviced more than once.

The properties mentioned thus far phrase the correctness requirement as a guarantee that the program must always provide. Such properties are called safety properties, since they stipulate that “for any sort of behaviour that the program can do, nothing bad ever happens.” As a consequence of this condition, showing that a program violates a safety property entails finding just one instance of a program execution that exhibits bad behaviour. Producing this evidence is enough of a proof that the program under scrutiny is not safe with respect to the property in question.

The next section explains how these properties can be expressed in a logic that precisely and unambiguously establishes the behaviour programs must comply with.