08.09.2012 - Patrick Michel

Uhrzeit 15:00 Uhr
Ort 34-420


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.

termine/ss12/120809.txt · Last modified: 05.11.2012 16:42 by paddy