Abstract
Taking advantage of recent advances in automated theorem proving, we present a new method for determining whether database transactions preserve integrity constraints. We consider check constraints and referential-integrity constraints—extracted from SQL table declarations—and application-level invariants expressed as formulas of first-order logic. Our motivation is to use static analysis of database transactions at development time, to catch bugs early, or during deployment, to allow only integrity-preserving stored procedures to be accepted. We work in the setting of a functional multi-tier language, where functional code is compiled to SQL that queries and updates a relational database. We use refinement types to track constraints on data and the underlying database. Our analysis uses a refinement-type checker, which relies on recent highly efficient SMT algorithms to check proof obligations. Our method is based on a list-processing semantics for an SQL fragment within the functional language, and is illustrated by a series of examples.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baltopoulos, I.G., Borgström, J., Gordon, A.D.: Maintaining database integrity with refinement types. Technical Report MSR–TR–2011–51, Microsoft Research (2011)
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Benedikt, M., Griffin, T., Libkin, L.: Verifiable properties of database transactions. Information and Computation 147(1), 57–88 (1998)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: Computer Security Foundations Symposium (CSF 2008), pp. 17–32. IEEE, Los Alamitos (2008)
Benzaken, V., Doucet, A.: Thémis: A database programming language handling integrity constraints. VLDB Journal 4, 493–517 (1995)
Bierman, G.M., Gordon, A.D., Hriţcu, C., Langworthy, D.: Semantic subtyping with an SMT solver. In: International Conference on Functional Programming (ICFP), pp. 105–116. ACM, New York (2010)
Borgström, J., Bhargavan, K., Gordon, A.D.: A compositional theory for STM Haskell. In: Haskell Symposium, pp. 69–80. ACM, New York (2009)
Borgström, J., Gordon, A.D., Pucella, R.: Roles, stacks, histories: A triple for Hoare. Journal of Functional Programming 21, 159–207 (2011); An abridged version of this article was published in A. W. Roscoe, Cliff B. Jones, Kenneth R. Wood (eds.), Reflections on the Work of C.A.R. Hoare, Springer London Ltd (2010)
Casanova, M.A., Bernstein, P.A.: A formal system for reasoning about programs accessing a relational database. ACM Transactions on Programming Languages and Systems 2(3), 386–414 (1980)
Chlipala, A.J.: Ur: statically-typed metaprogramming with type-level record computation. In: Programming Language Design and Implementation (PLDI), pp. 122–133. ACM, New York (2010)
Cooper, E., Lindley, S., Yallop, J.: Links: Web programming without tiers. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4709, pp. 266–296. Springer, Heidelberg (2007)
Dasgupta, A., Narasayya, V.R., Syamala, M.: A static analysis framework for database applications. In: International Conference on Data Engineering (ICDE), pp. 1403–1414. IEEE Computer, Los Alamitos (2009)
Filliâtre, J.-C.: Proof of imperative programs in type theory. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 78–92. Springer, Heidelberg (1999)
Flanagan, C.: Hybrid type checking. In: ACM Symposium on Principles of Programming Languages (POPL 2006), pp. 245–256 (2006)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI), pp. 234–245 (2002)
Gardarin, G., Melkanoff, M.A.: Proving consistency of database transactions. In: Fifth International Conference on Very Large Data Bases, pp. 291–298. IEEE, Los Alamitos (1979)
Krishnamurthi, S., Hopkins, P.W., Mccarthy, J., Graunke, P.T., Pettyjohn, G., Felleisen, M.: Implementation and use of the PLT scheme web server. Journal of Higher-Order and Symbolic Computing (HOSC) 20(4), 431–460 (2007)
Malecha, J.G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: Principles of Programming Languages (POPL), pp. 237–248. ACM, New York (2010)
Meijer, E., Beckman, B., Bierman, G.M.: LINQ: reconciling object, relations and XML in the.NET framework. In: SIGMOD Conference, p. 706. ACM, New York (2006)
Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: International Conference on Functional Programming (ICFP 2008), pp. 229–240. ACM, New York (2008)
Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An overview of the Scala programming language. Technical Report IC/2004/64, EPFL (2004)
Peyton Jones, S., Wadler, P.: Comprehensive comprehensions. In: Haskell 2007, pp. 61–72. ACM, New York (2007)
Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2 (2006)
Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: Programming Language Design and Implementation (PLDI), pp. 159–169. ACM, New York (2008)
Serrano, M., Gallesio, E., Loitsch, F.: Hop: a language for programming the web 2.0. In: Object-oriented programming systems, languages, and applications (OOPSLA 2006), pp. 975–985. ACM, New York (2006)
Sheard, T., Stemple, D.: Automatic verification of database transaction safety. ACM Transactions on Database Systems 14(3), 322–368 (1989)
Swamy, N., Chen, J., Chugh, R.: Enforcing stateful authorization and information flow policies in fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 529–549. Springer, Heidelberg (2010)
Syme, D., Granicz, A., Cisternino, A.: Expert F#. Apress (2007)
Wadler, P.: Comprehending monads. Mathematical Structures in Computer Science 2, 461–493 (1992)
Wadler, P.: Functional programming: An angry half-dozen. In: Cluet, S., Hull, R. (eds.) DBPL 1997. LNCS, vol. 1369, pp. 25–34. Springer, Heidelberg (1998)
Xi, H.: Dependent ML: An approach to practical programming with dependent types. Journal of Functional Programming 17(2), 215–286 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baltopoulos, I.G., Borgström, J., Gordon, A.D. (2011). Maintaining Database Integrity with Refinement Types. In: Mezini, M. (eds) ECOOP 2011 – Object-Oriented Programming. ECOOP 2011. Lecture Notes in Computer Science, vol 6813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22655-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-22655-7_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22654-0
Online ISBN: 978-3-642-22655-7
eBook Packages: Computer ScienceComputer Science (R0)