×

A relation-algebraic approach to the “Hoare logic” of functional dependencies. (English) Zbl 1434.68144

Summary: Abstract algebra has the power to unify seemingly disparate theories once they are encoded into the same abstract formalism. This paper shows how a relation-algebraic rendering of both database dependency theory and Hoare programming logic purports one such unification, in spite of the latter being an algorithmic theory and the former a data theory.The approach equips relational data with functional types and an associated type system which is useful for database operation type checking and optimization.
The prospect of a generic, unified approach to both programming and data theories on top of libraries already available in automated deduction systems is envisaged.

MSC:

68P15 Database theory
03B70 Logic in computer science
03G15 Cylindric and polyadic algebras; relation algebras
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

RelView; ESC/Java
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Schmidt, G., Relational Mathematics, (Encyclopedia of Mathematics and Its Applications, vol. 132 (2010), Cambridge University Press)
[2] Feferman, S., Tarski’s influence on computer science, Log. Methods Comput. Sci., 2 (2006), 1-1-13 · Zbl 1126.03005
[3] Bussche, J., Applications of Alfred Tarski’s ideas in database theory, (CSL’01: Proceedings of the 15th International Workshop on Computer Science Logic (2001), Springer-Verlag: Springer-Verlag London, UK), 20-37 · Zbl 0999.68055
[4] Maier, D., The Theory of Relational Databases (1983), Computer Science Press · Zbl 0519.68082
[5] Abiteboul, S.; Hull, R.; Vianu, V., Foundations of Databases (1995), Addison-Wesley · Zbl 0848.68031
[6] Tarski, A.; Givant, S., A Formalization of Set Theory without Variables, AMS Colloquium Publications, vol. 41 (1987), American Mathematical Society: American Mathematical Society Providence, Rhode Island · Zbl 0654.03036
[7] Struth, G., Isabelle repository for relational and algebraic methods (2011), URL:
[8] Höfner, P.; Struth, G., Automated reasoning in Kleene algebra, (Proceedings, CADE-21 (2007), Springer-Verlag), 279-294 · Zbl 1184.68462
[9] Beeri, C.; Fagin, R.; Howard, J., A complete axiomatization for functional and multivalued dependencies in database relations, (Smith, D., Proc. 1977 ACM SIGMOD, Toronto (1977), ACM: ACM NY, USA), 47-61
[10] Flanagan, C.; Leino, K.; Lillibridge, M.; Nelson, G.; Saxe, J.; Stata, R., Extended static checking for Java, (PLDI (2002)), 234-245
[11] Hoare, C., An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969), 583 · Zbl 0179.23105
[12] Mili, A.; Desharnais, J.; Gagné, J., Strongest invariant functions: Their use in the systematic analysis of while statements, Acta Inform., 22, 47-66 (1985) · Zbl 0546.68011
[13] Hoare, C.; Jifeng, H., Unifying Theories of Programming, Series in Computer Science (1998), Prentice-Hall International
[14] Oliveira, J., Pointfree foundations for (generic) lossless decomposition (2011), HASLab/INESC TEC & U. Minho, URL:
[15] Oliveira, J., Extended Static Checking by Calculation using the Pointfree Transform, LNCS, vol. 5520, 195-251 (2009), Springer-Verlag · Zbl 1250.68093
[16] Freyd, P.; Scedrov, A., Categories, Allegories, Mathematical Library, vol. 39 (1990), North-Holland · Zbl 0698.18002
[17] Doornbos, H.; Backhouse, R.; van der Woude, J., A calculational approach to mathematical induction, Theor. Comput. Sci., 179, 103-135 (1997) · Zbl 0901.68124
[18] Kozen, D., Kleene algebra with tests, ACM Trans. Program. Lang. Syst., 19, 427-443 (1997)
[19] Kozen, D., On Hoare logic and Kleene algebra with tests, ACM Trans. Comput. Log., 1, 60-76 (2000) · Zbl 1365.68326
[20] Desharnais, J.; Möller, B.; Struth, G., Kleene algebra with domain, ACM Trans. Comput. Log., 7, 798-833 (2006) · Zbl 1367.68205
[21] Wehrman, I.; Hoare, C.; O’Hearn, P. W., Graphical models of separation logic, Inf. Process. Lett., 109, 1001-1004 (2009) · Zbl 1200.68153
[22] Hoare, C.; He, J., The weakest prespecification, Inf. Process. Lett., 24, 127-132 (1987) · Zbl 0622.68025
[23] Bird, R.; de Moor, O., Algebra of Programming, Series in Computer Science (1997), Prentice-Hall International · Zbl 0867.68042
[24] Frias, M.; Baum, G.; Haeberer, A., Fork algebras in algebra, logic and computer science, Fundam. Inform., 1-25 (1997) · Zbl 0890.03036
[25] Wisnesky, R., Minimizing Monad comprehensions (2011), Harvard University: Harvard University Cambridge, Massachusetts, Technical Report TR-02-11
[26] Schmidt, G.; Ströhlein, T., Relations and Graphs: Discrete Mathematics for Computer Scientists, EATCS Monographs on Theoretical Computer Science (1993), Springer-Verlag · Zbl 0900.68328
[27] Jaoua, A.; Belkhiter, N.; Ounalli, H.; Moukam, T., Databases, (Brink, C.; Kahl, W.; Schmidt, G., Relational Methods in Computer Science (1997), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. New York, NY, USA), 197-210 · Zbl 0884.68045
[28] Okuma, H.; MacCaull, W.; Kawahara, Y., Informational representability for contexts in Dedekind categories (2003), Kyushu University, URL: · Zbl 1270.68104
[29] Oliveira, J., Towards a linear algebra of programming, Form. Asp. Comput., 24, 433-458 (2012) · Zbl 1259.68135
[30] Wong, S.; Butz, C., The implication of probabilistic conditional independence and embedded multivalued dependency, (8th Conf. on Inf. Processing and Management of Uncertainty in K.-B. Systems. 8th Conf. on Inf. Processing and Management of Uncertainty in K.-B. Systems, IPMU00 (2000)), 876-881
[31] Barthe, G.; Grégoire, B.; Béguelin, S., Probabilistic relational Hoare logics for computer-aided security proofs, (MPC’12 (2012)), 1-6 · Zbl 1358.94059
[32] Berghammer, R., Computing and visualizing Banks sets of dominance relations using relation algebra and RelView, J. Log. Algebr. Program., 82, 123-136 (2013) · Zbl 1278.91049
[33] Möller, B.; Roocks, P.; Endres, M., An algebraic calculus of database preferences, (MPC 2012. MPC 2012, LNCS, vol. 7342 (2012), Springer: Springer Berlin, Heidelberg), 241-262 · Zbl 1358.68087
[34] Oliveira, J.; Ferreira, M., Alloy meets the algebra of programming: A case study, IEEE Trans. Softw. Eng., 39, 305-326 (2013)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.