Rewriting

The main activity of VerCors is rewriting a program. We use the concept of a Rewriter to structure the transformation of a program tree in an understandable and disciplined manner.

A rewriter recurses into one tree, and calls dispatch for each element of the tree by default. To ensure that each part of the tree is actually rewritten, we use the concept of generations to make the prior tree and the new tree have unrelated types. Declarations are a bit special: each declaration need not be succeeded by exactly one declaration of the same kind — as opposed to structural nodes. By transforming a program tree the verification failures that may occur in the program change, so we explain how to transform the errors to be about the input by providing blames.

The later sections describe concepts that are more advanced, and require careful consideration to whether they are appropriate. Nested rewriters can be used when the rewriting behaviour materially changes when recursing into a certain node. It can be confusing to read, because you might intuit that the patterns in the parent rewriter are still used, when they are not. Substitution can be helpful if your rewriting process is effectively two-step, but it is more straightforward to glue on a simple behavior to one rewriter. Nevertheless it is often actually better to consider explicitly how you might model the substitution statefully anyway: this gives a clearer picture what should happen when e.g. nodes needing subtitution are nested.