\begin{listing}[style=script,mathescape,numbers=none]
public class $SRName$CSP implements CSProcess {

  /* WRAPPER IMPLEMENTATION */

  private final Any2OneChannel $method_0$Channel;
  $\ldots$
  private final Any2OneChannel $method_N$Channel;
  // variable declaration for inner state of the resource
  $\ldots$
  // method's wrapper schema 
  public T$_i$ $method_i$(T$_1$ arg$_0$,..,T$_m$ arg$_m$) {
    //@ assume P && I
    One2OneChannel innerChannel = Channel.one2one();
    $method_i$Channel.out().write(
                     new Request(innerChannel,$<footprint>$));
    //if double send   
    //@ assert P && I && C;
    innerChannel.out.write($\ldots$);
    T$_1$ value = (T$_1$) innerChannel.in().read();
    //@ assert Q && I;
    return value
  }

  // method accessing/modifying shared resource's inner state
  protected T$_i$ inner$method_i$(T$_1$ arg$_1$,..,T$_m$ arg$_m$) {
    //@ assume P && C && I;
    $S$;
    //@ assert Q && I;
  }

  /* SERVER IMPLEMENTATION */
  $\ldots$
  private static final int METHOD$_1$ = 0;
  $\ldots$
  private static final int METHOD$_N$ = N;
  $\ldots$
  private final Queue<Request> method$_i$Requests;
  $\ldots$
  public void run() {
    Guard[] inputs={method$_i$Channel.in(),$\ldots$,method$_N$Channel.in()};
    Alternative services = new Alternative(inputs);
    int choice = 0;
    while (true) {
      choice = services.fairSelect();
      /*@ assume chosenService < guards.length && 
        @        chosenService >= 0 &&
        @        guards[chosenService].pending() > 0;
        @*/
      switch(choice){
        $\ldots$
        case METHOD$_i$: 
          //@ assume P
          method$_i$Requests.add((Request) method$_i$Channel.in());
          break;
        $\ldots$
      }
      boolean requestProcessed = true;
      while (requestProcessed) {
        requestProcessed = false;
        for $all$ $requests$ $list $ do {
          int queueSize = method$_k$Requests.size();
          for (int i = 0; i < queueSize; i++) {
            Request request = method$_k$Requests.poll(QUEUE_HEAD);

            if ($condition_k$ (request.getFootprint()) ) {
              //@ assume $I$ && $condition_k$ ==> $C$ ;
              ChannelInput chIn = request.getChannel().in();
              T values = (T)chIn.read();
              results= this.innerMethod$_k$(values); 
              //@ assume $I$ && $Q$ ;
              request.getChannel().out.write(results);
              requestProcessed = true; 
            } else {
              method$_k$Requests.offer(request);
            }
          }
        }
        //@ ensures $there$ $is$ $no$ $stored$ $thread$ $in$ $any$ $request$ $list$ $which$ $its$ $synchronization$ $condition$ $holds$
      }
    } // end while
  }// end run
}
\end{listing}