proc main() {
    while (...) {
      p1();
      p2();
    }
  }
  proc p1() {
    open();
    readContent();
  }
  proc p2() {
    startLog();
    readContent();
    stopLog();
    close();
  }
  proc readContent() {
    while (...) {
      if (...) {
        read();
      } else {
        print();
      }
    }
  }

Suppose we wish to describe program behavior by considering only traces as sequences of procedure invocations.

The set of traces of procedure readContent can be given by the regular expression

(read | print)*

When we have finite elements of traces and we have program with procedures, the meaning is given by a context-free grammar:

main ::= mainStart mainLoop mainEnd
mainLoop ::= empty | p1 p2 mainLoop
p1 ::= p1Start open readContent p1End
p2 ::= p2Start startLog readContent stopLog close p2End
readContent = readContentStart rcLoop readContentEnd
rcLoop = empty | read rcLoop | print rcLoop

We may be interested whether the program the protocols given by regular expressions:

• file usage protocol: (open (read+write)* close)*
• logging service protocol: (startLog stopLog)*

Other similar examples are sockets, locks, and other stateful interfaces.