Verifying and Generating WP Transformers for Procedures on Complex Data

We present the formalized theory of a weakest precondition calculus for procedures on complex data with integrity constraints. The theory defines the assertion language and the wp-transformer. It contains the proofs for soundness and “weakestness” of the preconditions. Furthermore, we formalize a normalization process that eliminates all elementary updates from preconditions. This normalization property is important for efficient checking of the preconditions in programs. The theory is completely realized in Isabelle/HOL and used for generating the Haskell implementation of the wp-transformer and the normalization process.

The wp generation is developed for procedures on complex data with integrity constraints, for example XML documents satisfying a schema. Efficient checkability allows maintaining the constraints with acceptable computing resources. It is a central motivation of our work and has influenced many design decisions.