{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T05:19:03Z","timestamp":1737523143960,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441441"},{"type":"electronic","value":"9783540457190"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45719-4_1","type":"book-chapter","created":{"date-parts":[[2007,10,9]],"date-time":"2007-10-09T14:55:00Z","timestamp":1191941700000},"page":"1-14","source":"Crossref","is-referenced-by-count":5,"title":["From Specifications to Code in Casl"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Donald","family":"Sannella","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Br\u00fcckner, P. Mosses, D. Sannella and A. Tarlecki. Casl: The common algebraic specification language. Theoretical Computer Science, 2003. To appear.","DOI":"10.1016\/S0304-3975(01)00368-1"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"S. Autexier, D. Hutter, H. Mantel and A. Schairer. System description: INKA 5.0\u2014a logic voyager. Proc. 16th Intl. Conf. on Automated Deduction. Springer LNAI 1632, 207\u2013211, 1999.","DOI":"10.1007\/3-540-48660-7_15"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"E. Astesiano, B. Krieg-Br\u00fcckner and H.-J. Kreowski, editors. Algebraic Foundations of Systems Specification. Springer, 1999.","DOI":"10.1007\/978-3-642-59851-7"},{"key":"1_CR4","unstructured":"D. Aspinall. Type Systems for Modular Programming and Specification. PhD thesis, University of Edinburgh, 1997."},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"E. Bainbridge","year":"1990","unstructured":"E. Bainbridge, P. Freyd, A. Scedrov and P. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35\u201364, 1990.","journal-title":"Theoretical Computer Science"},{"key":"1_CR6","unstructured":"R. Burstall and P. Landin. Programs and their proofs: An algebraic approach. B. Meltzer and D. Michie, editors, Machine Intelligence 4, 17\u201343. Edinburgh University Press, 1969."},{"key":"1_CR7","unstructured":"M. Bidoit and P. Mosses. A gentle introduction to Casl. Tutorial, WADT\/CoFI Workshop at ETAPS 2001, Genova. Available from http:\/\/www.lsv.ens-cachan.fr\/~bidoit\/CASL\/ , 2001."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"M. Bidoit, D. Sannella and A. Tarlecki. Architectural specifications in Casl. Formal Aspects of Computing, 2002. To appear.","DOI":"10.1007\/s001650200012"},{"key":"1_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Global development via local observational construction steps","author":"M. Bidoit","year":"2002","unstructured":"M. Bidoit, D. Sannella and A. Tarlecki. Global development via local observational construction steps. Proc. 27th Intl. Symp. on Mathematical Foundations of Computer Science, Warsaw. Springer LNCS, 2002. To appear."},{"key":"1_CR10","unstructured":"CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible from http:\/\/www.brics.dk\/Projects\/CoFI\/ ."},{"key":"1_CR11","unstructured":"CoFI Language Design Task Group. Casl\u2014The CoFI Algebraic Specification Language\u2014Summary, version 1.0.1. http:\/\/Documents\/CASL\/v1.0.1\/Summary , in [CoF], 2001."},{"key":"1_CR12","unstructured":"CoFI Semantics Task Group. Casl\u2014The CoFI Algebraic Specification Language\u2014Semantics, version 1.0. http:\/\/Documents\/CASLSemantics , in [CoF], 2002."},{"key":"1_CR13","unstructured":"D. Detlefs, K. R. M. Leino, G. Nelson and J. Saxe. Extended static checking. Technical Report #159, Compaq SRC, Palo Alto, USA, 1998."},{"key":"1_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-59293-8_188","volume-title":"Testing can be formal, too","author":"M.-C. Gaudel","year":"1995","unstructured":"M.-C. Gaudel. Testing can be formal, too. Intl. Joint Conf. on Theory and Practice of Software Development (TAPSOFT\u201995), Aarhus. Springer LNCS 915, 82\u201396, 1995."},{"key":"1_CR15","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J. Goguen","year":"1992","unstructured":"J. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the Assoc. for Computing Machinery, 39:95\u2013146, 1992.","journal-title":"Journal of the Assoc. for Computing Machinery"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"J. Goguen and G. Ro\u015fu. Institution morphisms. Formal Aspects of Computing, 2002. To appear.","DOI":"10.1007\/s001650200013"},{"key":"1_CR17","unstructured":"M. Kohlhase. OMDoc: An open markup format for mathematical documents, version 1.1. Available from http:\/\/www.mathweb.org\/omdoc\/index.html , 2002."},{"key":"1_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/BFb0053589","volume-title":"Reflections on the design of a specification language","author":"S. Kahrs","year":"1998","unstructured":"S. Kahrs and D. Sannella. Reflections on the design of a specification language. Proc. Intl. Colloq. on Fundamental Approaches to Software Engineering. European Joint Conferences on Theory and Practice of Software (ETAPS\u201998), Lisbon. Springer LNCS 1382, 154\u2013170, 1998."},{"key":"1_CR19","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML: A gentle introduction. Theoretical Computer Science, 173:445\u2013484, 1997.","journal-title":"Theoretical Computer Science"},{"key":"1_CR20","unstructured":"G. Leavens, A. Baker and C. Ruby. Preliminary design of JML. Technical Report TR #98-06p, Department of Computer Science, Iowa State University, 2001."},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"G. Leavens, K. R. M. Leino, E. Poll, C. Ruby and B. Jacobs. JML: notations and tools supporting detailed design in Java. OOPSLA 2000 Companion, Minneapolis, 105\u2013106, 2000.","DOI":"10.1145\/367845.367996"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"J. Meseguer. General logics. Logic Colloquium\u201987, 275\u2013329. North Holland, 1989.","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"1_CR23","unstructured":"E. Meijer and J. Gough. A technical overview of the commmon language infrastructure. Available from http:\/\/research.microsoft.com\/~emeijer\/Papers\/CLR.pdf , 2001(?)."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"F. Morris. Advice on structuring compilers and proving them correct. Proc. 3rd ACM Symp. on Principles of Programming Languages, 144\u2013152. ACM Press, 1973.","DOI":"10.1145\/512927.512941"},{"key":"1_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-46419-0_8","volume-title":"Casl: From semantics to tools","author":"T. Mossakowski","year":"2000","unstructured":"T. Mossakowski. Casl: From semantics to tools. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), European Joint Conferences on Theory and Practice of Software, Berlin. Springer LNCS 1785, 93\u2013108, 2000."},{"key":"1_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/978-3-540-44616-3_15","volume-title":"Recent Trends in Algebraic Development Techniques: Selected Papers from WADT\u201999","author":"T. Mossakowski","year":"2000","unstructured":"T. Mossakowski. Specification in an arbitrary institution with symbols. Recent Trends in Algebraic Development Techniques: Selected Papers from WADT\u201999, Bonas. Springer LNCS 1827, 252\u2013270, 2000."},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"T. Mossakowski. Relating Casl with other specification languages: the institution level. Theoretical Computer Science, 2003. To appear.","DOI":"10.1016\/S0304-3975(01)00369-3"},{"key":"1_CR28","series-title":"Lect Notes Comput Sci","volume-title":"Unit testing for Casl architectural specifications","author":"P. Machado","year":"2002","unstructured":"P. Machado and D. Sannella. Unit testing for Casl architectural specifications. Proc. 27th Intl. Symp. on Mathematical Foundations of Computer Science, Warsaw. Springer LNCS, 2002. To appear."},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"1_CR30","unstructured":"T. Nipkow, D. von Oheimb and C. Pusch. \u03ceJava: Embedding a programming language in a theorem prover. F. L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation. Proc. Intl. Summer School Marktoberdorf 1999, 117\u2013144. IOS Press, 2000."},{"key":"1_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1007\/BFb0037118","volume-title":"A logic for parametric polymorphism","author":"G. Plotkin","year":"1993","unstructured":"G. Plotkin and M. Abadi. A logic for parametric polymorphism. Proc. of the Intl. Conf. on Typed Lambda Calculi and Applications, Amsterdam. Springer LNCS 664, 361\u2013375, 1993."},{"key":"1_CR32","unstructured":"R. Boulton, A. Gordon, M. Gordon, J. Herbert and J. van Tassel. Experience with embedding hardware description languages in HOL. Proc. of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, 129\u2013156. North-Holland, 1992."},{"key":"1_CR33","series-title":"Lect Notes Comput Sci","volume-title":"HasCasl: Towards integrated specification and development of haskell programs","author":"L. Schr\u00f6der","year":"2002","unstructured":"L. Schr\u00f6der and T. Mossakowski. HasCasl: Towards integrated specification and development of haskell programs. Proc. 9th Intl. Conf. on Algebraic Methodology And Software Technology, Reunion. Springer LNCS, this volume, 2002."},{"key":"1_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/3-540-61550-4_143","volume-title":"Mind the gap! Abstract versus concrete models of specifications","author":"D. Sannella","year":"1996","unstructured":"D. Sannella and A. Tarlecki. Mind the gap! Abstract versus concrete models of specifications. Proc. 21st Intl. Symp. on Mathematical Foundations of Computer Science, Cracow. Springer LNCS 1113, 114\u2013134, 1996."},{"key":"1_CR35","unstructured":"A. Tarlecki. Towards heterogeneous specifications. D. Gabbay and M. van Rijke, editors, Proc. of the Intl. Conf. on Frontiers of Combining Systems (FroCoS\u201998), 337\u2013360. Research Studies Press, 2000."},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"P. Wadler. Theorems for free! Proc. of the 4th Intl. Conf. on Functional Programming and Computer Architecture. ACM Press, 1989.","DOI":"10.1145\/99370.99404"},{"issue":"5","key":"1_CR37","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/173668.168635","volume":"27","author":"R. Wahbe","year":"1993","unstructured":"R. Wahbe, S. Lucco, T. Anderson and S. Graham. Efficient software-based fault isolation. ACM SIGOPS Operating Systems Review, 27(5):203\u2013216, December 1993.","journal-title":"ACM SIGOPS Operating Systems Review"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45719-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T13:59:05Z","timestamp":1737467945000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45719-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441441","9783540457190"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-45719-4_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}