class WebTax authority(Preparer) {           // Scott D. Stoller, 12nov2007

  TaxRules{Preparer:Preparer} rules = ...

  // handle tax preparation request from principal p.
  // addr: address for connections with principal p
  // the method's begin PC label {p:p} is a lower bound 
  // for the method's side-effects.
  // info about the method arguments flows to the output channel with label
  // {p:p}, so we label the arguments with {p:p}.
  handleRequest{p:p}(principal{p:p} p, Address{p:p} addr) 
    where authority(Preparer) {

    // note: treatment of input and output streams is simplified.
    InputStream{p:p} in = new InputStream(addr, {p:p});
    // assuming the TaxData constructor cannot throw exceptions, the label
    // of the "new" expression and hence of the "data" variable is based on
    // the PC label here, which is bounded by {p:p} based on this method's 
    // begin PC label and the preceding statements.
    TaxData[p]{p:p} data = new TaxData[p](in);

    // labels are like primitive values, not like references, so the label
    // for lb depends on the PC label and the labels of p and Preparer.
    final label{p:p} lb = new label{Preparer:Preparer; p:p};
    TaxForm[p, lb]{p:p} f = new TaxForm[p, lb]();
    f.prepare(data, rules);
    String{*lb} s = f.toString();
    String{p:p} s2 = declassify(s, {*lb} to {p:p});
    OutputStream{p:p} out = new OutputStream(addr, {p:p});
    out.write(s2);
  }
}

// p: the customer whose tax data this is
class TaxData[principal p] {
  int{p:p} income;
  int{p:p} withholding;
  ...

  // read data from "in" and use it to initialize this object
  TaxData[p](InputStream{p:p} in) { ... }
}

class TaxRules {
  ... // field declarations omitted

  String{Preparer:Preparer; p:p} compute(TaxData[p] d, int lineNumber) { ... }
}

// p: the customer whose tax form this is
// lb: label to use for information that depends on p's tax data and
//  on the Preparer's proprietary tax preparation rules.
class TaxForm[principal p, label lb]

  // values for filling in the blank lines on tax form
  String{lb} line1;
  String{lb} line2;
  ...

  void prepare{lb}(TaxData{p:p} data, TaxRules{Preparer:Preparer} rules) {
    line1 = rules.compute(d, 1);
    line2 = rules.compute(d, 2);
    ...
  }

  String{lb} toString() {...}
}