Mirco Dotta, Philippe Suter, and Viktor Kuncak.
On static analysis for expressive pattern matching.
Technical Report LARA-REPORT-2008-004, EPFL, 2008.
Pattern matching is a widespread programming language
construct that enables definitions of values by cases,
generalizing if-then-else and case statements. The cases in
a pattern matching expression should be exhaustive: when the
value does not match any of the cases, the expression throws
a run-time exception. Similarly, each pattern should be
reachable, and, if possible, patterns should be disjoint to
facilitate reasoning. Current compilers use simple analyses
to check patterns. Such analyses ignore pattern guards,
use static types to approximate possible
expression values, and do not take into account properties
of user-defined functions.
We present a design and implementation of a new analysis of
pattern matching expressions. Our analysis detects a wider
class of errors and reports fewer false alarms than previous
approaches. It checks disjointness, reachability, and
exhaustiveness of patterns by expressing these conditions as
formulas and proving them using decision procedures and
theorem provers. It achieves precision by propagating
possible values through nested expressions and approximating
pattern-matching guards with formulas. It supports
user-defined “extractor” functions in patterns by relying
on specifications of relationships between the domains of
such functions. The result is the first analysis that
enables verified, declarative pattern matching with guards
in the presence of data abstraction. We have implemented
our analysis and describe our experience in checking a range
of pattern matching expressions in a subset of the Scala
programming language.
[ bib ]
Back