Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Appel, A.W., Blazy, S.: Separation Logic for Small-Step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)
Barbosa, D., et al.: Efficient incremental validation of XML documents. In: ICDE 2004, pp. 671–682. IEEE Computer Society, Washington, DC, USA (2004)
Bouchou, B., Alves, M.H.F.: Updates and Incremental Validation of XML Documents. In: Lausen, G., Suciu, D. (eds.) DBPL 2003. LNCS, vol. 2921, pp. 216–232. Springer, Heidelberg (2004)
Buneman, P., et al.: Constraints for semistructured data and XML. SIGMOD Rec. 30, 47–54 (2001)
Buneman, P., et al.: Keys for XML. In: WWW 2001, pp. 201–210. ACM, Hong Kong (2001)
Buneman, P., Davidson, S.B., Fan, W., Hara, C., Tan, W.C.: Reasoning about Keys for XML. In: Ghelli, G., Grahne, G. (eds.) DBPL 2001. LNCS, vol. 2397, pp. 133–148. Springer, Heidelberg (2002)
Calcagno, C., Dinsdale-Young, T.: Decidability of context logic (2009)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. In: POPL 2005, pp. 271–282. ACM, Long Beach (2005)
Cheney, J., Urban, C.: Mechanizing the Metatheory of mini-XQuery. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 280–295. Springer, Heidelberg (2011)
Clark, J.: RELAX NG compact syntax (November 2002), http://www.oasis-open.org/committees/relax-ng/compact-20021121.html
Gardner, P.A., et al.: Local hoare reasoning about dom. In: PODS 2008, pp. 261–270. ACM, Vancouver (2008)
Gries, D.: The Science of Programming. Springer (1981)
Michel, P., Fillibeck, C.: Stats - softech achievement tracking system (2011), http://xcend.de/stats/start
Michel, P., Poetzsch-Heffter, A.: Assertion support for manipulating constrained data-centric XML. In: PLAN-X 2009 (January 2009)
Michel, P., Poetzsch-Heffter, A.: Maintaining XML Data Integrity in Programs - An Abstract Datatype Approach. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds.) SOFSEM 2010. LNCS, vol. 5901, pp. 600–611. Springer, Heidelberg (2010)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
von Oheimb, D.: Hoare logic for java in Isabelle/HOL. Concurrency and Computation: Practice and Experience 13(13), 1173–1214 (2001)
Papakonstantinou, Y., Vianu, V.: Incremental Validation of XML Documents. In: Calvanese, D., Lenzerini, M., Motwani, R. (eds.) ICDT 2003. LNCS, vol. 2572, pp. 47–63. Springer, Heidelberg (2002)
Schirmer, N.: A Verification Environment for Sequential Imperative Programs in Isabelle/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 398–414. Springer, Heidelberg (2005)
Vogels, F., Jacobs, B., Piessens, F.: A machine-checked soundness proof for an efficient verification condition generator. In: Symposium on Applied Computing, vol. 3, pp. 2517–2522. ACM (March 2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Michel, P., Poetzsch-Heffter, A. (2012). Verifying and Generating WP Transformers for Procedures on Complex Data. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-32347-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32346-1
Online ISBN: 978-3-642-32347-8
eBook Packages: Computer ScienceComputer Science (R0)