Copyright and Licensing
Articles accepted for publication will be licensed under the Creative Commons BY-NC. Authors must sign a non-exclusive distribution agreement after article acceptance.
Computer Aided Verification of Relational Models by Strategic Rewriting
DOI:
https://doi.org/10.24215/16666038.17.e19Keywords:
models verification, symbolic execution, abstract model verification, extended static checking, strategic term rewritingAbstract
Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based modeling and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations such as database queries, state transitions, or composition of functional components. When data models, their constraints and operations are represented by point-free binary relational expressions, proof obligations can be expressed as inclusions between relational expressions. We developed a typedirected, strategic term rewriting system that can be used to simplify relational proof obligations and ultimately reduce them to tautologies. Such reductions can be used to provide extended static checking for design contraints commonly found in software modeling and development.
Downloads
Download data is not yet available.
References
[1] J. Fitzgerald and P. Larsen, Modelling Systems: Practical Tools and Tech. for Soft. Development . Cambridge University Press, 1st ed., 1998.
[2] C. Jones, Systematic Software Development Using VDM. Series in Computer Science, PrenticeHall International, 1986. C.A. R. Hoare.
[3] K. Leino, “Extended static checking: A tenyear perspective,” in Informatics - 10 Years Back. 10 Years Ahead., pp. 157–175, Springer-Verlag, 2001.
[4] C. Flanagan, K. Leino, M. Lillibridge, G. Nelson, J. Saxe, and R. Stata, “Extended static checking for Java.,” in PLDI, pp. 234–245, 2002.
[5] D. Detlefs, G. Nelson, and J. Saxe, “Simplify: a theorem prover for program checking.,” J. ACM, vol. 52, no. 3, pp. 365–473, 2005.
[6] J. Oliveira and C. Rodrigues, “Pointfree factorization of operation refinement,” in FM’06, vol. 4085 of LNCS, pp. 236–251, SpringerVerlag, 2006.
[7] J. Oliveira, “Extended static checking by calculation using the PF-transform,” Jul. 2008. LerNET’08 post-workshop tutorial paper submitted for publication.
[8] E. Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5, pp. 357–361. Berlin, Heidelberg: Springer Berlin Heidelberg, 2001.
[9] R. Lämmel and J. Visser, “A Strafunski Application Letter,” in PADL’03 (V. Dahl et al., eds.), vol. 2562 of LNCS, pp. 357–375, Springer, 2003.
[10] R. Lämmel, E. Visser, and J. Visser, “The Essence of Strategic Programming.” 2002.
[11] E. Kreyszig, Advanced Engineering Mathematics. J.Wiley & Sons, Inc., 1988.
[12] R. Bird and O. de Moor, Algebra of Programming. Series in Computer Science, Prentice-Hall International, 1997. C.A.R. Hoare, series editor.
[13] A. Cunha and J. Visser, “Strongly typed rewriting for coupled software transformation,” Electron. Notes Theor. Comput. Sci., vol. 174, no. 1, pp. 17–34, 2007.
[14] P. Silva and J. Oliveira, “’Galculator’: functional prototype of a Galois-connection based proof assistant,” in PPDP ’08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, (New York, NY, USA), pp. 44–55, ACM, 2008.
[15] J. Oliveira and C. Rodrigues, “Transposing relations: from Maybe functions to hash tables,” in MPC’04, vol. 3125 of LNCS, pp. 334–356, Springer, 2004.
[16] B. MacLennan, “Overview of relational programming.,” SIGPLAN Not., vol. 18, no. 3, pp. 36–45, 1983.
[17] D. Cattrall and C. Runciman, “Widening the representation bottleneck: a functional implementation of relational programming,” in Proc. Func. Prog. Lang. and Comp. Arch., pp. 191–200, ACM Press, 1993.
[2] C. Jones, Systematic Software Development Using VDM. Series in Computer Science, PrenticeHall International, 1986. C.A. R. Hoare.
[3] K. Leino, “Extended static checking: A tenyear perspective,” in Informatics - 10 Years Back. 10 Years Ahead., pp. 157–175, Springer-Verlag, 2001.
[4] C. Flanagan, K. Leino, M. Lillibridge, G. Nelson, J. Saxe, and R. Stata, “Extended static checking for Java.,” in PLDI, pp. 234–245, 2002.
[5] D. Detlefs, G. Nelson, and J. Saxe, “Simplify: a theorem prover for program checking.,” J. ACM, vol. 52, no. 3, pp. 365–473, 2005.
[6] J. Oliveira and C. Rodrigues, “Pointfree factorization of operation refinement,” in FM’06, vol. 4085 of LNCS, pp. 236–251, SpringerVerlag, 2006.
[7] J. Oliveira, “Extended static checking by calculation using the PF-transform,” Jul. 2008. LerNET’08 post-workshop tutorial paper submitted for publication.
[8] E. Visser, Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5, pp. 357–361. Berlin, Heidelberg: Springer Berlin Heidelberg, 2001.
[9] R. Lämmel and J. Visser, “A Strafunski Application Letter,” in PADL’03 (V. Dahl et al., eds.), vol. 2562 of LNCS, pp. 357–375, Springer, 2003.
[10] R. Lämmel, E. Visser, and J. Visser, “The Essence of Strategic Programming.” 2002.
[11] E. Kreyszig, Advanced Engineering Mathematics. J.Wiley & Sons, Inc., 1988.
[12] R. Bird and O. de Moor, Algebra of Programming. Series in Computer Science, Prentice-Hall International, 1997. C.A.R. Hoare, series editor.
[13] A. Cunha and J. Visser, “Strongly typed rewriting for coupled software transformation,” Electron. Notes Theor. Comput. Sci., vol. 174, no. 1, pp. 17–34, 2007.
[14] P. Silva and J. Oliveira, “’Galculator’: functional prototype of a Galois-connection based proof assistant,” in PPDP ’08: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, (New York, NY, USA), pp. 44–55, ACM, 2008.
[15] J. Oliveira and C. Rodrigues, “Transposing relations: from Maybe functions to hash tables,” in MPC’04, vol. 3125 of LNCS, pp. 334–356, Springer, 2004.
[16] B. MacLennan, “Overview of relational programming.,” SIGPLAN Not., vol. 18, no. 3, pp. 36–45, 1983.
[17] D. Cattrall and C. Runciman, “Widening the representation bottleneck: a functional implementation of relational programming,” in Proc. Func. Prog. Lang. and Comp. Arch., pp. 191–200, ACM Press, 1993.
Downloads
Published
2017-10-01
How to Cite
Necco, C. M., Oliveira, J. N., Visser, J., & Uzal, R. (2017). Computer Aided Verification of Relational Models by Strategic Rewriting. Journal of Computer Science and Technology, 17(02), e19. https://doi.org/10.24215/16666038.17.e19
Issue
Section
Invited Articles
