Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
verifying_pattern_matching_with_guards [2007/06/21 10:21] mirco.dotta |
verifying_pattern_matching_with_guards [2007/06/30 01:19] philippe.suter |
||
---|---|---|---|
Line 2: | Line 2: | ||
** Mirco Dotta, Philippe Suter ** | ** Mirco Dotta, Philippe Suter ** | ||
- | ===== Documents ===== | + | Abstract from the final report: |
- | * slides for printing {{1xdotta_suter_presentation.pdf|}} (without animation) | + | ---- |
- | * slides for the presentation{{dotta_suter_presentation.pdf|}} | + | 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.) | ||
+ | * Don't forget to read the [[http://sav07.googlecode.com/svn/trunk/README|README file]] before trying to run the implementation. | ||
+ | * slides for printing {{1xverify_pattern_matching1.1.pdf|}} (without animation) | ||
+ | * slides for presentation{{verify_pattern_matching1.1.pdf|}} |