Mirco Dotta, Philippe Suter

Abstract from the final report:

Pattern matching is a powerful construct for conditional execution, and is present in many programming languages, particularly in functional ones. The number and complexity of patterns in a matching expression often grows quickly as programs are written, and the task of checking the completeness or disjointness of such an expression becomes tedious. Compilers can assist programmers to some extent, but complex cases, such as the use of guards to refine the patterns, are in general too difficult to deal with and are hence treated very conservatively. As a result, no useful information can be gained from the compilation process and programmers, once more, have to resort to manual checking of their expressions.

In this project, we show how formal verification techniques can be used to prove completeness or disjointess of a pattern matching expression with guards. Our examples and results are based on the Scala programming language [1], but we believe they can be extended to other languages with a minimal amount of work.

[1] http://scala-lang.org

• The final report is available here.
• Sources of the implementation are available through Google code: http://code.google.com/p/sav07/source.

(Note that this also includes the .tex source files for the report and the presentation.)

• Don't forget to read the README file before trying to run the implementation.
• slides for printing 1xverify_pattern_matching1.1.pdf (without animation)
• slides for presentationverify_pattern_matching1.1.pdf