Verifying pattern matching with guards

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.


Documents and sources

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