====== The FunCheck Scala Compiler Plugin ======

See also: [[projects::funcheck]] for the general ideas.



===== Flow =====

{{projects:plugin-flow.jpg|Flow}}

Stages of the plugin:

=== Symbol Table ===

Generation of a minimalistic symbol table from the CompilationUnits (and with storing pointers to the entries in the actual ''scalac'' symbol table), where we store classes, objects, possibly traits, and their methods.

=== Contract Extraction ===

Application of pattern matching to recover the ''require'' and ''ensuring'' contracts. (Does not need to be explicitely separated from the following phase.) We should stop if the contracts are not expressed in [[funcheck-purescala|Pure Scala]], and generate the proper Pure Scala trees otherwise.

=== Code Extraction ===

Generation of [[funcheck-lightscala|Light Scala]] (or, for now, [[funcheck-purescala|Pure Scala]]) trees from the ''scalac'' AST.

=== Verification Conditions ===

Generation of VCs following the usual assume/guarantee principle. Additionally to pre/post-conditions, we can generate VCs for:
  * pattern matching exhaustiveness (= runtime MatchException)

=== Discharging ===

Call to an SMT solver, hopefully with a formula in a QF theory.

=== (Optionally) Counter-Example Generation ===

Unclear.