PROGRAMMER’S VIEWPOINT OF CONTRACTS. FOR SESSIONS In this section we provide a programmer’s viewpoint of contracts for sessions using the process networks depicted in Figure 1 as running examples. In these networks, the aim of module User is to obtain an element w resulting from two elements v1, v2 produced by Source and combined by Operator. For the sake of illustration, we assume that all the elements are integer numbers and that w = v1 mod v2. According to the network on the left-hand side of Figure 1, User establishes two sessions x and y with Source and Operator respectively, it forwards every element vi received from x on y, and receives the transformed element w from y. Session types allow us to formalize these protocols specifying the type, direction and order of messages exchanged within sessions. In this case, the session endpoints x and y owned by User are typed as x : ?int.?int.end and y : !int.!int.?int.end. In words, User uses x to receive two integer numbers and y to send two numbers and then to receive another one. What session types do not describe are additional requirements and guarantees concerning the content of exchanged messages. In this scenario, for example, it could be sensible to specify that the second number sent from User to Operator should be different from zero and that the number sent from Operator to User is non negative. Such specifications – hereafter called contracts – could be used to monitor, at runtime, the interaction between User and Operator so as to detect contract violations and, hopefully, to guide programmers to the source of the problem. The approach of Findler and Xxxxxxxxx [2002] to contract monitoring rests on three key ingredients:
