{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:14:13Z","timestamp":1759637653331},"publisher-location":"Berlin, Heidelberg","reference-count":66,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642031526"},{"type":"electronic","value":"9783642031533"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03153-3_5","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T06:11:14Z","timestamp":1248675074000},"page":"195-251","source":"Crossref","is-referenced-by-count":13,"title":["Extended Static Checking by Calculation Using the Pointfree Transform"],"prefix":"10.1007","author":[{"given":"Jos\u00e9 N.","family":"Oliveira","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Aarts, C., Backhouse, R.C., Hoogendijk, P., Voermans, E., van der Woude, J.: A relational theory of datatypes (December 1992), www.cs.nott.ac.uk\/~rcb","DOI":"10.1007\/3-540-57499-9_15"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/11526841_27","volume-title":"FM 2005: Formal Methods","author":"T.L. Alves","year":"2005","unstructured":"Alves, T.L., Silva, P.F., Visser, J., Oliveira, J.N.: Strategic term rewriting and its application to a VDM-SL to SQL conversion. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 399\u2013414. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"5_CR3","first-page":"153","volume":"15","author":"K. Backhouse","year":"2004","unstructured":"Backhouse, K., Backhouse, R.C.: Safety of abstract interpretations for free, via logical relations and Galois connections. SCP\u00a015(1-2), 153\u2013196 (2004)","journal-title":"SCP"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/11783596_7","volume-title":"Mathematics of Program Construction","author":"R. Backhouse","year":"2006","unstructured":"Backhouse, R., Michaelis, D.: Exercises in quantifier manipulation. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 70\u201381. Springer, Heidelberg (2006)"},{"key":"5_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-1-4612-4476-9_2","volume-title":"Beauty is our business: a birthday salute to Edsger","author":"R.C. Backhouse","year":"1990","unstructured":"Backhouse, R.C.: On a relation on functions. In: Dijkstra, W. (ed.) Beauty is our business: a birthday salute to Edsger, New York, NY, USA, pp. 7\u201318. Springer, Heidelberg (1990)"},{"key":"5_CR6","unstructured":"Backhouse, R.C.: Fixed point calculus. In: Summer School and Workshop on Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Lincoln College, Oxford, UK, April 10-14 (2000)"},{"key":"5_CR7","unstructured":"Backhouse, R.C.: Mathematics of Program Construction. Univ. of Nottingham. Draft of book in preparation, 608 pages (2004)"},{"key":"5_CR8","first-page":"303","volume-title":"AMAST 1991","author":"R.C. Backhouse","year":"1992","unstructured":"Backhouse, R.C., de Bruin, P., Hoogendijk, P., Malcolm, G., Voermans, T.S., van der Woude, J.: Polynomial relators. In: AMAST 1991, pp. 303\u2013362. Springer, Heidelberg (1992)"},{"issue":"4","key":"5_CR9","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1017\/S096012950000030X","volume":"3","author":"R.C. Backhouse","year":"1993","unstructured":"Backhouse, R.C., Woude, J.: Demonic operators and monotype factors. Mathematical Structures in Computer Science\u00a03(4), 417\u2013433 (1993)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"8","key":"5_CR10","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/359576.359579","volume":"21","author":"J. Backus","year":"1978","unstructured":"Backus, J.: Can programming be liberated from the von Neumann style? a functional style and its algebra of programs. CACM\u00a021(8), 613\u2013639 (1978)","journal-title":"CACM"},{"issue":"1","key":"5_CR11","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2006.07.030","volume":"365","author":"L.S. Barbosa","year":"2006","unstructured":"Barbosa, L.S., Oliveira, J.N.: Transposing partial components \u2014 an exercise on coalgebraic refinement. Theoretical Computer Science\u00a0365(1), 2\u201322 (2006)","journal-title":"Theoretical Computer Science"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-79980-1_7","volume-title":"Algebraic Methodology and Software Technology","author":"L.S. Barbosa","year":"2008","unstructured":"Barbosa, L.S., Oliveira, J.N., Silva, A.M.: Calculating invariants as coreflexive bisimulations. In: Meseguer, J., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol.\u00a05140, pp. 83\u201399. Springer, Heidelberg (2008)"},{"key":"5_CR13","series-title":"Series in Computer Science","volume-title":"Algebra of Programming","author":"R. Bird","year":"1997","unstructured":"Bird, R., de Moor, O.: Algebra of Programming. Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1997) C.A.R. Hoare (series editor)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Bove, A., Dybjer, P.: Dependent types at work. Lecture Notes for the LerNet Summer School, Piriapolis, Uruguay, 47 p. (Feburary 2008)","DOI":"10.1007\/978-3-642-03153-3_2"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Claessen, K., Hughes, J.: Quickcheck: a lightweight tool for random testing of Haskell programs. In: ICFP, pp. 268\u2013279 (2000)","DOI":"10.1145\/351240.351266"},{"key":"5_CR16","unstructured":"Intel Corporation. Intel Flash File System Core Reference Guide. Doc. Ref. 304436-001 (October 2004)"},{"key":"5_CR17","unstructured":"CSK. The Integrity Checking: Using Proof Obligations (2007)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/11813040_20","volume-title":"FM 2006: Formal Methods","author":"A. Cunha","year":"2006","unstructured":"Cunha, A., Oliveira, J.N., Visser, J.: Type-safe two-level data transformation. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 284\u2013299. Springer, Heidelberg (2006)"},{"key":"5_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate calculus and program semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer, New York (1990)"},{"issue":"1-2","key":"5_CR20","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos","year":"1997","unstructured":"Doornbos, H., Backhouse, R., van der Woude, J.: A calculational approach to mathematical induction. Theoretical Computer Science\u00a0179(1-2), 103\u2013135 (1997)","journal-title":"Theoretical Computer Science"},{"key":"5_CR21","unstructured":"Ferreira, M.A., Silva, S.S., Oliveira, J.N.: Verifying Intel FLASH file system core specification. In: Modelling and Analysis in VDM: Proceedings of the Fourth Overture\/VDM++ Workshop at FM 2008, Turku, Finland, May 26, 2008. University of Newcastle, Computer Science. Technical Report CS-TR-1099 (2008)"},{"key":"5_CR22","volume-title":"Modelling Systems: Practical Tools and Techniques for Software Development","author":"J. Fitzgerald","year":"1998","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques for Software Development, 1st edn. Cambridge University Press, Cambridge (1998)","edition":"1"},{"key":"5_CR23","volume-title":"Validated Designs for Object\u2013oriented Systems","author":"J. Fitzgerald","year":"2005","unstructured":"Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object\u2013oriented Systems. Springer, New York (2005)"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"5_CR25","series-title":"Mathematical Library","volume-title":"Categories, Allegories","author":"P.J. Freyd","year":"1990","unstructured":"Freyd, P.J., \u0160\u010dedrov, A.: Categories, Allegories. Mathematical Library, vol.\u00a039. North-Holland, Amsterdam (1990)"},{"key":"5_CR26","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"issue":"10","key":"5_CR27","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM\u00a012(10), 576\u2013580 (1969)","journal-title":"CACM"},{"key":"5_CR28","unstructured":"Hoare, C.A.R., Misra, J.: Verified software: theories, tools, experiments \u2014 vision of a Grand Challenge project. In: Proceedings of IFIP working conference on Verified Software: theories, tools, experiments (2005)"},{"key":"5_CR29","unstructured":"Hoogendijk, P.: A Generic Theory of Data Types. PhD thesis, University of Eindhoven, The Netherlands (1997)"},{"key":"5_CR30","volume-title":"Software abstractions: logic, language, and analysis","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software abstractions: logic, language, and analysis. MIT Press, Cambridge (2006)"},{"key":"5_CR31","unstructured":"Jacobs, B.: Introduction to Coalgebra. Towards Mathematics of States and Observations. Draft Copy. Institute for Computing and Information Sciences, Radboud University Nijmegen, P.O. Box 9010, 6500 GL Nijmegen, The Netherlands"},{"key":"5_CR32","series-title":"Series in Computer Science","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1986","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 1st edn. Series in Computer Science. Prentice-Hall Int., Englewood Cliffs (1986) (1990)","edition":"1"},{"key":"5_CR33","unstructured":"Peyton Jones, S.L.: Haskell 98 Language and Libraries. Cambridge University Press, Cambridge (2003); also published as a Special Issue of the Journal of Functional Programming 13(1) (Janurary 2003)"},{"issue":"2","key":"5_CR34","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/s00165-006-0022-3","volume":"19","author":"R. Joshi","year":"2007","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Formal Asp. Comput.\u00a019(2), 269\u2013272 (2007)","journal-title":"Formal Asp. Comput."},{"issue":"2","key":"5_CR35","first-page":"275","volume":"27","author":"Y. Kawahara","year":"1973","unstructured":"Kawahara, Y.: Notes on the universality of relational functors. Mem. Fac. Sci. Kyushu Univ (Series A, Mathematics)\u00a027(2), 275\u2013289 (1973)","journal-title":"Mem. Fac. Sci. Kyushu Univ. (Series A, Mathematics)"},{"issue":"1","key":"5_CR36","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. Trans. Computational Logic\u00a01(1), 60\u201376 (2000)","journal-title":"Trans. Computational Logic"},{"key":"5_CR37","volume-title":"Advanced Engineering Mathematics","author":"E. Kreyszig","year":"1988","unstructured":"Kreyszig, E.: Advanced Engineering Mathematics, 6th edn. J.\u00a0Wiley & Sons, Chichester (1988)","edition":"6"},{"key":"5_CR38","unstructured":"Maier, D.: The Theory of Relational Databases. Computer Science Press (1983)"},{"issue":"10","key":"5_CR39","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Computer\u00a025(10), 40\u201351 (1992)","journal-title":"IEEE Computer"},{"key":"5_CR40","first-page":"62","volume-title":"ICFP 2006","author":"A. Nanevski","year":"2006","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: ICFP 2006, pp. 62\u201373. ACM, New York (2006)"},{"key":"5_CR41","unstructured":"Necco, C., Oliveira, J.N., Visser, J.: ESC\/PF: Static checking of relational models by calculation (2008) (submitted)"},{"issue":"8","key":"5_CR42","first-page":"754","volume":"7","author":"J.N. Oliveira","year":"2001","unstructured":"Oliveira, J.N.: Bagatelle in C arranged for VDM SoLo. JUCS\u00a07(8), 754\u2013781 (2001)","journal-title":"JUCS"},{"key":"5_CR43","unstructured":"Oliveira, J.N.: Constrained datatypes, invariants and business rules: a relational approach. PUReCaf\u00e9 talk, DI-UM, 2004.5.20, PURe Project (POSI\/CHS\/44304\/2002) (2004)"},{"key":"5_CR44","unstructured":"Oliveira, J.N.: Calculate databases with \u2018simplicity\u2019. Presentation at the IFIP WG 2.1 #59 Meeting, Nottingham, UK (September 2004) (slides available from the author\u2019s website)"},{"key":"5_CR45","unstructured":"Oliveira, J.N.: Data dependency theory made generic \u2014 by calculation. Presentation at the IFIP WG 2.1 #62 Meeting, Namur, Belgium (December 2006)"},{"key":"5_CR46","unstructured":"Oliveira, J.N.: Reinvigorating pen-and-paper proofs in VDM: the pointfree approach. In: Presented at the Third Overture Workshop, Newcastle, UK, November 27-28 (2006)"},{"key":"5_CR47","unstructured":"Oliveira, J.N.: Pointfree foundations for (generic) lossless decomposition (2008) (submitted)"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-88643-3_4","volume-title":"Generative and Transformational Techniques in Software Engineering II","author":"J.N. Oliveira","year":"2008","unstructured":"Oliveira, J.N.: Transforming Data by Calculation. In: L\u00e4mmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2007. LNCS, vol.\u00a05235, pp. 134\u2013195. Springer, Heidelberg (2008)"},{"key":"5_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-27764-4_18","volume-title":"Mathematics of Program Construction","author":"J.N. Oliveira","year":"2004","unstructured":"Oliveira, J.N., Rodrigues, C.J.: Transposing relations: from Maybe functions to hash tables. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 334\u2013356. Springer, Heidelberg (2004)"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/11813040_17","volume-title":"FM 2006: Formal Methods","author":"J.N. Oliveira","year":"2006","unstructured":"Oliveira, J.N., Rodrigues, C.J.: Pointfree factorization of operation refinement. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 236\u2013251. Springer, Heidelberg (2006)"},{"key":"5_CR51","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1090\/S0002-9947-1944-0010555-7","volume":"55","author":"O. Ore","year":"1944","unstructured":"Ore, O.: Galois connexions. Trans. Amer. Math. Soc.\u00a055, 493\u2013513 (1944)","journal-title":"Trans. Amer. Math. Soc."},{"key":"5_CR52","volume-title":"Types and programming languages","author":"B.C. Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)"},{"key":"5_CR53","first-page":"248","volume-title":"Proc. of the 7th Annual IEEE Symp. on Logic in Computer Science","author":"V. Pratt","year":"1992","unstructured":"Pratt, V.: Origins of the calculus of binary relations. In: Proc. of the 7th Annual IEEE Symp. on Logic in Computer Science, Santa Cruz, CA, pp. 248\u2013254. IEEE Comp. Soc., Los Alamitos (1992)"},{"key":"5_CR54","first-page":"513","volume":"83","author":"J.C. Reynolds","year":"1983","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. Information Processing\u00a083, 513\u2013523 (1983)","journal-title":"Information Processing"},{"key":"5_CR55","volume-title":"The Forgotten Revolution: How Science Was Born in 300BC and Why It Had to Be Reborn","author":"L. Russo","year":"2003","unstructured":"Russo, L.: The Forgotten Revolution: How Science Was Born in 300BC and Why It Had to Be Reborn. Springer, Heidelberg (2003)"},{"key":"5_CR56","first-page":"44","volume-title":"PPDP 2008: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming","author":"P.F. Silva","year":"2008","unstructured":"Silva, P.F., Oliveira, J.N.: \u2018Galculator\u2019: functional prototype of a Galois-connection based proof assistant. In: PPDP 2008: Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming, pp. 44\u201355. ACM, New York (2008)"},{"key":"5_CR57","series-title":"Series in Computer Science","volume-title":"The Z Notation \u2014 A Reference Manual","author":"J.M. Spivey","year":"1989","unstructured":"Spivey, J.M.: The Z Notation \u2014 A Reference Manual. Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1989) C.A.R. Hoare (series editor)"},{"key":"5_CR58","unstructured":"Open Group\u00a0Technical Standard. Standard for information technology - Portable operating system interface (POSIX). System interfaces. IEEE Std 1003.1, 2004 edn. The Open Group Technical Standard. Base Specifications, Issue 6. Includes IEEE Std 1003.1-2001, IEEE Std 1003.1-2001\/Cor 1-2002 and IEEE Std 1003.1-2001\/Cor 2-2004. System Interfaces (2004)"},{"key":"5_CR59","doi-asserted-by":"crossref","unstructured":"Takano, A., Meijer, E.: Shortcut to deforestation in calculational form. In: Proc. FPCA 1995 (1995)","DOI":"10.1145\/224164.224221"},{"key":"5_CR60","series-title":"American Mathematical Society","volume-title":"A Formalization of Set Theory without Variables","author":"A. Tarski","year":"1987","unstructured":"Tarski, A., Givant, S.: A Formalization of Set Theory without Variables. American Mathematical Society, vol.\u00a041. AMS Colloquium Publications, Providence (1987)"},{"key":"5_CR61","unstructured":"Vermolen, S.D.: Automatically discharging VDM proof obligations using HOL. Master\u2019s thesis, Radboud University Nijmegen, Computing Science Department (June-August 2007)"},{"key":"5_CR62","unstructured":"Voermans, T.S.: Inductive Datatypes with Laws and Subtyping \u2014 A Relational Model. PhD thesis, University of Eindhoven, The Netherlands (1999)"},{"key":"5_CR63","first-page":"13","volume-title":"Symposium on Partial Evaluation and Semantics-Based Program Manipulation","author":"J. Voigtl\u00e4nder","year":"2008","unstructured":"Voigtl\u00e4nder, J.: Proving correctness via free theorems: The case of the destroy\/build-rule. In: Gl\u00fcck, R., de Moor, O. (eds.) Symposium on Partial Evaluation and Semantics-Based Program Manipulation, San Francisco, California, Proceedings, pp. 13\u201320. ACM Press, New York (2008)"},{"key":"5_CR64","first-page":"347","volume-title":"4th International Symposium on Functional Programming Languages and Computer Architecture","author":"P.L. Wadler","year":"1989","unstructured":"Wadler, P.L.: Theorems for free! In: 4th International Symposium on Functional Programming Languages and Computer Architecture, London, pp. 347\u2013359. ACM, New York (1989)"},{"key":"5_CR65","first-page":"263","volume-title":"TASE 2008","author":"S. Wang","year":"2008","unstructured":"Wang, S., Barbosa, L.S., Oliveira, J.N.: A Relational Model for Confined Separation Logic. In: TASE 2008, pp. 263\u2013270. IEEE Computer Society, Los Alamitos (2008)"},{"key":"5_CR66","volume-title":"Using Z: Specification, Refinement, and Proof","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc., Upper Saddle River (1996)"}],"container-title":["Lecture Notes in Computer Science","Language Engineering and Rigorous Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03153-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T04:24:07Z","timestamp":1685075047000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03153-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642031526","9783642031533"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03153-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}