Synchronization contracts: an example of syntax

I'd like to introduce very briefly the syntax of synchronization contracts.
As we have seen in the previuos two posts, we use them to express

assertions on temporal behaviour
synchronization

In the first group we have three keywords, mutated from DbC (those familiar with the concept will be at home here): requires, ensures and invariant.

In the second group, we have the variants of preconditions and postconditions we introduced last time: requires_wait and ensures_wait. In the base form of a synchonization contract language, these keywords are all we need. Well, plus the LTL keywords, of course.
Their meaning is pretty obvious: for a complete introduction, see chapter 5 of my thesis. Here I will introduce only some of them:

pre(cond): cond was true at the previous step
once(cond): cond was true once
cond1 since cond2: cond2 became true, and from that moment cond1 was true also
cond1 until cond2: cond1 must hold until cond2 is true

These operators will be useful to express conditions on the flow of the program: the first three are PLTL operators, the last one is a classical LTL operator.

class Stream
{
    bool ready;
    invariant(@recevive -> (!@send until @endReceive));
    invariant(@receive -> finally(endReceive));

    void init();

    void receive()
       requires(ready && once(@init));
    void endReceive()
    void send()
    void endSend()  
}

Pretty simple, huh? the @method construct is used to express the concept "the method has been executed", and is a pretty shortcut for not introducing a ton of state variables. Here synchronization contracts are used to specify behaviour, and to check it. But let's see another example:

public class HistoryBuffer
{
   invariant(current == max -> (!@Put until @Get));

   public virtual object Get()
      requires_wait(current > 0);

   public virtual object Get()
      requires_wait(current < max);
   {
      --current;
      object ret = buf[current];
      return ret;
   }
   public virtual object GGet()
      requires_wait(pre(@Put))
   {
      return Get();
   }
}

Now we have chacks (the invariant) and also synchronization (the guards on Put, Get and GGet). The GGet function have the requirement to be executed only if the previous operation is a Put (i.e. it does not permit two subsequent Get operations). See how it is simple to express such a concept, much simpler than with a stadard programming language.
Next time we'll see an interesting synchronization problem and how it can be solved with synchronization contracts.