Differences

This shows you the differences between two versions of the page.

--- verifying_pattern_matching_with_guards [2007/06/21 14:41]
mirco.dotta
+++ verifying_pattern_matching_with_guards [2007/06/30 00:59]
philippe.suter
@@ Line 2: / Line 2: @@
 ** Mirco Dotta, Philippe Suter **
-===== Documents =====
+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]]
+----
+===== Documents and sources =====
+  * The final report is available [[http://icwww.epfl.ch/~psuter/report.pdf|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.
   * slides for printing {{1xverify_pattern_matching1.1.pdf|}} (without animation)
   * slides for presentation{{verify_pattern_matching1.1.pdf|}}