Lab for Automated Reasoning and Analysis LARA

Code examples extracted from the scala libraries/compiler

Here is a collection from pattern matching expressions found in the scala libraries, or in the compiler. Many of them are of limited interest, but could be used later on for suggesting improvements on verifiability, for examples by adding invariants and the like. Note that there are many more examples to be found there, but most of them were not collected, because they fell in one of the following patterns:

  • match on Some(n) / None. Option is sealed, and the completeness is already checked by the compiler.. Disjointness/irredundancy is obvious
  • match on something-really-precise (eg. Seq('X','M','L')..) and then a wildcard. Used to throw exceptions occasionnally. Not that interesting.
  • use of match to define equals.

From the libraries

From src/library/scala/io/BytePickle.scala. I was just wondering why the Nil case is not treated (and hence the need for @unchecked).

def listToPair(l: List[a]): (a,List[a]) =
    (l: @unchecked) match { case x :: xs => (x, xs) }

From src/library/scala/io/Source.scala. Every one likes side-effects…

/** returns next character and has the following side-effects: updates
 *  position (ccol and cline) and assigns the character to ch
def next = {
    ch =
    pos = Position.encode(cline,ccol)
    ch match {
        case '\n' =>
            ccol = 1
            cline += 1
        case '\t' =>
            ccol += tabinc
        case _ =>
            ccol += 1

From src/library/scala/ref/ReferenceQueue.scala. Matching on a Java class.

def Wrapper(ref: java.lang.ref.Reference) = ref match {
    case null => None
    case ref => new Wrapper(ref)

From src/library/scala/xml/ContentModel.scala. Apparently, the function collects all labels present in a regular expression. The interesting thing is that RegExp has many more subclasses than that (see after the code), so how does the author know that they won't appear? Maybe something to be put in preconditions/invariants.

 def getLabels(r: RegExp): scala.collection.Set[String] = {
    val s = new scala.collection.mutable.HashSet[String]()
    def traverse1(xs: Seq[RegExp]) {
      val it = xs.elements
      while (it.hasNext) traverse(
    def traverse(r: RegExp) {
      r match { // !!! check for match translation problem
        case Letter(ElemName(name)) => s += name
        case Star(  x @ _  ) => traverse( x ) // bug if x@_*
        case Sequ( xs @ _* ) => traverse1(xs)
        case Alt(  xs @ _* ) => traverse1(xs)
    return s

Subclasses from RegExp (in the same directory… the class is not sealed, btw).

Base.scala:  case class Alt(rs: _regexpT*)  extends RegExp {
Base.scala:  case class Sequ(rs: _regexpT*) extends RegExp {
Base.scala:  case class Star(r: _regexpT) extends RegExp {
Base.scala:  case object Eps extends RegExp {
Base.scala:  class Meta(r1: _regexpT) extends RegExp {
PointedHedgeExp.scala:  case class  Node(label: _labelT, r: _regexpT) extends RegExp {
PointedHedgeExp.scala:  case class  TopIter(r1: _regexpT, r2: _regexpT) extends RegExp {
PointedHedgeExp.scala:  case object Point extends RegExp {
WordExp.scala:  case class Letter(a: _labelT) extends RegExp {
WordExp.scala:  case class Wildcard() extends RegExp {

In the same file, a good old sealed class with a complete match.

  def toString(c: ContentModel, sb: StringBuilder): StringBuilder = c match {
    case ANY =>
    case EMPTY =>
    case PCDATA =>
    case ELEMENTS( _ ) | MIXED( _ ) =>

Summarized class hierarchy..

sealed abstract class ContentModel { ... }
case object PCDATA extends ContentModel { ... }
case object EMPTY extends ContentModel { ... }
case object ANY extends ContentModel { ... }

sealed abstract class DFAContentModel extends ContentModel { ... }
case class MIXED(r:ContentModel.RegExp) extends DFAContentModel { ... }
case class  ELEMENTS(r:ContentModel.RegExp) extends DFAContentModel { ... }

In src/library/scala/xml/dtd/Tokens.scala. Match on integers. Not that exciting, really, but where's the guarantee that it will never be called with anything larger outside [0:13]…

  final def token2string(i: Int): String = i match {
    case 0 => "#PCDATA"
    case 1 => "NAME"
    case 3 => "("
    case 4 => ")"
    case 5 => ","
    case 6 => "*"
    case 7 => "+"
    case 8 => "?"
    case 9 => "|"
    case 10 => "END"
    case 13 => " "

In src/library/scala/xml/Utility.scala. Sounds like someone wants preconditions to be respected.. Now wouldn't that be so much easier with predicate dispatch.

  /** trims an element - call this method, when you know that it is an
   *  element (and not a text node) so you know that it will not be trimmed
   *  away. With this assumption, the function can return a Node,
   *  rather than a Seq[Node]. If you don't know, call
   *  trimProper and account for the fact that you may get back
   *  an empty sequence of nodes.
   *  precondition: node is not a text node (it might be trimmed)
  def trim(x:Node): Node = x match {
    case Elem(pre,lab,md,scp,child@_*) =>
      Elem(pre,lab,md,scp, (child flatMap trimProper):_*)

From src/library/scala/xml/parsing/MarkupParser.scala. So ch only holds 'S' or 'P' when this is called.. Precondition? class invariant?

  /** holds the next character */
  var ch: Char = _
  /** externalID ::= SYSTEM S syslit
   *                 PUBLIC S pubid S syslit
  def externalID(): ExternalID = ch match {
    case 'S' =>
      val sysID = systemLiteral()
      new SystemID(sysID)
    case 'P' =>
      nextch; xToken("UBLIC")
      val pubID = pubidLiteral()
      val sysID = systemLiteral()
      new PublicID(pubID, sysID)

In fact, it is explicitely checked before it's called. See:

    //external ID
    if ('S' == ch || 'P' == ch) {
      extID = externalID()


    ch match {
      case 'S' | 'P' => //sy
        val extID = externalID()

(and another couple of times)

Now, verify this. Looks complete to me. I'm not sure how pattern subsumption verification would be useful here: seems to me like this would issue a lot of warnings because of the potential collisions between every single one and the first one. From src/library/scala/text/Document.scala. Note that there is another similar example in the file (without the initial 'guarded wildcard').

case object DocNil extends Document
case object DocBreak extends Document
case class DocText(txt: String) extends Document
case class DocGroup(doc: Document) extends Document
case class DocNest(indent: Int, doc: Document) extends Document
case class DocCons(hd: Document, tl: Document) extends Document
abstract class Document {
  def format(width: Int, writer: Writer) {
    type FmtState = (Int, Boolean, Document)
    def fits(w: Int, state: List[FmtState]): Boolean = state match {
      case _ if w < 0 =>
      case List() =>
      case (_, _, DocNil) :: z =>
        fits(w, z)
      case (i, b, DocCons(h, t)) :: z =>
        fits(w, (i,b,h) :: (i,b,t) :: z)
      case (_, _, DocText(t)) :: z =>
        fits(w - t.length(), z)
      case (i, b, DocNest(ii, d)) :: z =>
        fits(w, (i + ii, b, d) :: z)
      case (_, false, DocBreak) :: z =>
        fits(w - 1, z)
      case (_, true, DocBreak) :: z =>
      case (i, _, DocGroup(d)) :: z =>
        fits(w, (i, false, d) :: z)

From scalacheck

ScalaCheck is interesting for (almost) toy-sized examples. It uses almost exclusively sealed classes for pattern matching, and all its (6) source files compile without any warning. So it could be interesting as an example to show that our verifications are at least as good as scalac's.

From sttracker

(sttracker) Nothing interesting there. Too small.

codefromscala.txt · Last modified: 2007/08/16 15:19 by philippe.suter