{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,20]],"date-time":"2023-02-20T10:17:46Z","timestamp":1676888266581},"reference-count":69,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80932-0","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"51-93","source":"Crossref","is-referenced-by-count":7,"title":["Refinement and Development of Programs from Relational Specifications"],"prefix":"10.1016","volume":"44","author":[{"given":"Wolfram","family":"Kahl","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB1","unstructured":"Aarts C., R. C. Backhouse, P. Hoogendijk, E. Voermans and J. van der Woude, A relational theory of datatypes, Working document (1992), 387 pp., available at http:\/\/www.cs.nott.ac.uk\/~rcb\/MPC\/book.ps.gz."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB2","doi-asserted-by":"crossref","unstructured":"Abrial J.-R., \u201cThe B-Book: Assigning Programs to Meanings,\u201d Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB3","series-title":"Advanced functional programming: Third International School, AFP '98, Braga, Portugal, September 12\u201319, 1998: revised lectures","first-page":"28","article-title":"Generic programming. an introduction","author":"Backhouse","year":"1999"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB4","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S096012950000030X","article-title":"Demonic operators and monotype factors","volume":"3","author":"Backhouse","year":"1993","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB5","unstructured":"Barr M. and C. Wells, \u201cCategory Theory for Computing Science,\u201d Prentice Hall International Series in Computer Science, Prentice Hall, 1990."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Baum, G. A., M. F. Frias, A. M. Haeberer and P. Mart\u00ednez L\u00f3pez, From specifications to programs: A fork-algebraic approach to bridge the gap, in: Proceedings of Mathematical Foundations of Computer Science 1996 (MFCS '96), Cracow, Poland, LNCS 1113 (1996), pp. 180\u2013191.","DOI":"10.1007\/3-540-61550-4_147"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB7","series-title":"AMAST '93","first-page":"167","article-title":"Comparing two different approaches to products in abstract relation algebra","author":"Berghammer","year":"1994"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB8","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(86)90172-6","article-title":"Relational algebraic semantics of deterministic and nondeterministic programs","volume":"43","author":"Berghammer","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB9","series-title":"Constructive Methods in Computing Science","first-page":"151","article-title":"Lectures on constructive functional programming","author":"Bird","year":"1989"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB10","series-title":"\u201cAlgebra of Programming,\u201d","author":"Bird","year":"1997"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB11","series-title":"\u201cRelational Methods in Computer Science,\u201d","year":"1997"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB12","doi-asserted-by":"crossref","DOI":"10.1016\/S0167-6423(99)00005-2","article-title":"Bridging the algorithm gap: A linear-time functional program for paragraph formatting","volume":"35","author":"de Moor","year":"1999","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB13","series-title":"\u201cData Refinement: Model-Oriented Proof Methods and their Comparison,\u201d","author":"de Roever","year":"1998"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB14","series-title":"\u201cProc. RelMiCS 6, International Workshop on Relational Methods in Computer Science, Oisterwijk near Tilburg, Netherlands, 16\u201321 October 2001,\u201d","year":"2002"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB15","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/S0020-0255(99)00020-1","article-title":"Monomorphic characterization of n-ary direct products","volume":"119","author":"Desharnais","year":"1999","journal-title":"Information Sciences"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB16","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(94)00271-J","article-title":"Embedding a demonic semilattice in a relation algebra","volume":"149","author":"Desharnais","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB17","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0020-0255(01)00162-1","article-title":"Relational methods in computer science, special issue devoted to RelMiCS 5 in Valcartier, Qu\u00e9bec, January 2000","volume":"139","author":"Desharnais","year":"2001","journal-title":"Information Sciences"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB18","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0304-3975(93)90074-4","article-title":"A relational division operator: The conjugate kernel","volume":"114","author":"Desharnais","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB19","doi-asserted-by":"crossref","unstructured":"Desharnais J., A. Mili and T. T. Nguyen, Refinement and demonic semantics, in: Brink et al. [11] pp. 166\u2013183.","DOI":"10.1007\/978-3-7091-6510-2_11"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB20","doi-asserted-by":"crossref","unstructured":"Doornbos H., N. van Gasteren and R. Backhouse, Programs and datatypes, in: Brink et al. [11] pp. 150\u2013165.","DOI":"10.1007\/978-3-7091-6510-2_10"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB21","unstructured":"Frappier M., \u201cA Relational Basis for Program Construction by Parts,\u201d Ph.D. thesis, University of Ottawa, Computer Science Department, 150 Louis Pasteur, Ottawa, ON, K1N 6N5, Canada (1995)."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB22","series-title":"MCP '95","first-page":"257","article-title":"Program construction by parts","author":"Frappier","year":"1995"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB23","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0167-6423(95)00028-3","article-title":"A relational calculus for program construction by parts","volume":"26","author":"Frappier","year":"1996","journal-title":"Science of Computer Programming"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB24","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1093\/jigpal\/6.2.317","article-title":"Unifying program construction and modification","volume":"6","author":"Frappier","year":"1998","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB25","series-title":"\u201cCategories, Allegories,\u201d","first-page":"xviii+296","author":"Freyd","year":"1990"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-1997-32101","article-title":"Fork algebras in algebra, logic and computer science","volume":"32","author":"Frias","year":"1997","journal-title":"Fund. Inform"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB27","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1093\/jigpal\/6.2.227","article-title":"Representability and program construction within fork algebras","volume":"6","author":"Frias","year":"1998","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB28","article-title":"Relational methods in computer science, special issue devoted to RelMiCS 2 in Paraty, July 1995","volume":"6","author":"Haeberer","year":"1998","journal-title":"Journal of the IGPL"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB29","doi-asserted-by":"crossref","unstructured":"Haeberer A., M. Frias, G. Baum and P. Veloso, Fork algebras, in: Brink et al. [11] pp. 54\u201369.","DOI":"10.1007\/978-3-7091-6510-2_4"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB30","series-title":"Formal Methods in Programming and Their Applications, Proc. Internat. Conf. Novosibirsk, June 28\u2013July 3, 1993","first-page":"403","article-title":"On the smooth calculation of relational recursive expressions out of first-order non-constructive specifications involving quantifiers","author":"Haeberer","year":"1994"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB31","unstructured":"He J., C. A. R. Hoare and J. W. Sanders, Data refinement refined, in: B. Robinet and R. Wilhelm, editors, ESOP 86, European Symposium on Programming, LNCS 213 (1986), pp. 187\u2013196."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB32","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","article-title":"Proof of correctness of data representations","volume":"1","author":"Hoare","year":"1972","journal-title":"Acta Informatica"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB33","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/27651.27653","article-title":"Laws of programming","volume":"30","author":"Hoare","year":"1987","journal-title":"Comm. ACM"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB34","first-page":"51","article-title":"The weakest prespecification","volume":"4","author":"Hoare","year":"1986","journal-title":"Fund. Inform"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB35","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","article-title":"Prespecification in data refinement","volume":"25","author":"Hoare","year":"1987","journal-title":"Inform. Process. Lett"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB36","unstructured":"ISO\/IEC 13568: 2002, Information technology \u2013- Z formal specification notation \u2013- syntax, type system and semantics, international Standard."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB37","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/S0020-0255(99)00010-9","article-title":"Relational methods in computer science, special issue devoted to RelMiCS 3 in Hammamet, January 1997","volume":"119","author":"Jaoua","year":"1999","journal-title":"Information Sciences"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB38","doi-asserted-by":"crossref","unstructured":"Jipsen P., C. Brink and G. Schmidt, Background material, in: Brink et al. [11] pp. 1\u201321.","DOI":"10.1007\/978-3-7091-6510-2_1"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB39","series-title":"\u201cSoftware Development: A Rigorous Approach\u201d","author":"Jones","year":"1980"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB40","series-title":"\u201cSystematic Software Development Using VDM\u201d","author":"Jones","year":"1986"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB41","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/S0020-0255(01)00165-7","article-title":"Parallel composition and decomposition of specifications","volume":"139","author":"Kahl","year":"2001","journal-title":"Information Sciences"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB42","first-page":"275","article-title":"Notes on the universality of relational functors","volume":"27","author":"Kawahara","year":"1973","journal-title":"Mem. Fac. Sci. Kyushu Univ. Ser. A"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB43","series-title":"VDM '90: VDM and Z \u2013- Formal Methods in Software Development","first-page":"164","article-title":"Z and the refinement calculus","author":"King","year":"1990"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB44","doi-asserted-by":"crossref","first-page":"673","DOI":"10.1109\/32.940565","article-title":"Defining and applying measures of distance between specifications","volume":"27","author":"Jilani","year":"2001","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB45","unstructured":"Meertens L., Algorithmics: Towards programming as a mathematical activity, in: J. W. de Bakker, M. Hazewinkel and J. K. Lenstra, editors, Proc. CWI Symposium on Mathematics and Computer Science (1986), pp. 289\u2013334."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB46","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0304-3975(99)00085-7","article-title":"Semantic distance between specifications","volume":"247","author":"Mili","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB47","series-title":"Constructing Programs From Specifications","first-page":"319","article-title":"Relations as program development language","author":"M\u00f6ller","year":"1991"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB48","series-title":"\u201cBertrand Russell: Toward the \u201cPrinciples of Mathematics\u201d,\u201d","year":"1993"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB49","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","article-title":"A generalization of Dijkstra's calculus","volume":"11","author":"Nelson","year":"1989","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB50","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1007\/BF00263649","article-title":"Non-deterministic data types: Models and implementations","volume":"22","author":"Nipkow","year":"1986","journal-title":"Acta Informatica"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB51","series-title":"\u201cRelational Methods for Computer Science Applications,\u201d","year":"2001"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB52","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/358161.358168","article-title":"A generalized control structure and its formal definition","volume":"26","author":"Parnas","year":"1983","journal-title":"Comm. ACM"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB53","series-title":"13th World Computer Congress 94, Vol. 1: Technology and Foundations","first-page":"354","article-title":"Mathematical descriptions and specification of software","author":"Parnas","year":"1994"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB54","unstructured":"Parnas, D. L. and J. Madey, Functional documentation for computer systems engineering (version 2), Science of Computer Programming 25 (1995), pp. 41-61, also CRL Reports 237 and 309, McMaster Univ., Communications Research Laboratory and TRIO (Telecommunications Research Inst. of Ontario), Sept. 1991, pp. 14."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB55","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0012-365X(96)00043-X","article-title":"Closure lattices","volume":"154","author":"Pfaltz","year":"1996","journal-title":"Discrete Mathematics"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB56","first-page":"12","article-title":"Th\u00e9orie g\u00e9n\u00e9rale des s\u00e9ries bien-ordonn\u00e9es","volume":"VIII","author":"Russell","year":"1902","journal-title":"Rivista di Matematica"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB57","unstructured":"Russell B., \u201cIntroduction to Mathematical Philosophy,\u201d Routledge, 1919, reprinted 1998."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB58","unstructured":"Schmidt G., Programme als partielle Graphen, Habil. Thesis, Fachbereich Mathematik der Technischen Univ. M\u00fcnchen, Bericht 7813 (1977), English as [59,60]."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB59","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(81)90060-8","article-title":"Programs as partial graphs I: Flow equivalence and correctness","volume":"15","author":"Schmidt","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB60","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/0304-3975(81)90068-2","article-title":"Programs as partial graphs II: Recursion","volume":"15","author":"Schmidt","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB61","doi-asserted-by":"crossref","unstructured":"Schmidt G., C. Hattensperger and M. Winter, Heterogeneous relation algebra, in: Brink et al. [11] pp. 39\u201353.","DOI":"10.1007\/978-3-7091-6510-2_3"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB62","unstructured":"Schmidt G. and T. Str\u00f6hlein, \u201cRelations and Graphs, Discrete Mathematics for Computer Scientists,\u201d EATCS-Monographs on Theoretical Computer Science, Springer, 1993."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB63","series-title":"MCP '92","first-page":"302","article-title":"A calculus for predicative programming","author":"Sekerinski","year":"1992"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB64","unstructured":"Spivey, J. M., \u201cThe Z Notation: A Reference Manual,\u201d Prentice Hall International Series in Computer Science, Prentice-Hall, 1989, out of print; available via URL: http:\/\/spivey.oriel.ox.ac.uk\/~mike\/zrm\/."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB65","series-title":"ZUM'98, The Z Formal Specification Notation","first-page":"193","article-title":"Innovations in the notation of Standard Z","author":"Toyn","year":"1998"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB66","unstructured":"I. Tony, editor, \u201cZ Notation, Final Committee Draft, CD 13568.2,\u201d Developed by members of the Z Standards Panel, BSI Panel IST\/5\/-\/19\/2 (Z Notation), ISO Panel JTC1\/SC22\/WG19 (Rapporteur Group for Z), Project number JTC1.22.45, 1999, current version: Consensus Working Draft 2.7, October 12, 2001. URL: http:\/\/web.comlab.ox.ac.uk\/oucl\/research\/groups\/zstandards\/index.html."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB67","first-page":"52","article-title":"A finitary relational algebra for classical first-order logic","volume":"20","author":"Veloso","year":"1991","journal-title":"Bull. Polish Acad. Sci. Math., Sect. on Logic"},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB68","unstructured":"Winter M., \u201cStrukturtheorie heterogener Relationenalgebren mit Anwendung auf Nichtdeterminismus in Programmiersprachen,\u201d Ph.D. thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t der Bundeswehr M\u00fcnchen (1998)."},{"key":"10.1016\/S1571-0661(04)80932-0_NEWBIB69","series-title":"\u201cUsing Z: Specification, Refinement, and Proof,\u201d","author":"Woodcock","year":"1996"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104809320?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104809320?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:10:53Z","timestamp":1585897853000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104809320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":69,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1571066104809320"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80932-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}