{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,26]],"date-time":"2023-10-26T09:12:08Z","timestamp":1698311528842},"reference-count":25,"publisher":"Wiley","issue":"5","license":[{"start":{"date-parts":[[2006,10,30]],"date-time":"2006-10-30T00:00:00Z","timestamp":1162166400000},"content-version":"vor","delay-in-days":4200,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Pract Exp"],"published-print":{"date-parts":[[1995,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper advocates the use functional programming languages for the formal specification of (abstract) machines. The presented description method describes machines by a two\u2010level model. At the bottom layer machine components and the micro instructions to handle them are described by using an abstract data type. The top layer describes the machine instructions in terms of these micro instructions.<\/jats:p><jats:p>Using a functional language as specification language has several advantages. The abstraction mechanisms offered by a functional programming language are that good that one can abstract from irrelevant details as is required for a specification language. Functional languages have a well\u2010defined semantics such that the meaning of the specification is clear as well. Moreover, they offer the advantages of a programming language: the compiler can check the specification for partial correctness, eliminating for example type errors and unbound identifiers (errors which occur in many published descriptions). Furthermore, the specification can be executed such that one obtains a prototype implementation almost for free. Such an executable formal specification can, for instance, be used to investigate the dynamic behaviour of the described machine.<\/jats:p><jats:p>For a simple machine, the proposed description method is compared with several other description methods: a traditional style, a denotational semantics and a formal specification in the language Z. To show that the proposed method is indeed useful to describe large and complicated machines, the method is applied for the specification of an abstract imperative graph rewrite machine (the ABC\u2010machine) which has been used in the construction of the compiler for the functional language Concurrent Clean.<\/jats:p>","DOI":"10.1002\/spe.4380250502","type":"journal-article","created":{"date-parts":[[2006,11,17]],"date-time":"2006-11-17T18:01:43Z","timestamp":1163786503000},"page":"463-499","source":"Crossref","is-referenced-by-count":6,"title":["Operational machine specification in a functional programming language"],"prefix":"10.1002","volume":"25","author":[{"given":"P. W. M.","family":"Koopman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. C. J. D. Van","family":"Eekelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. J.","family":"Plasmeijer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2006,10,30]]},"reference":[{"key":"e_1_2_1_2_2","first-page":"2","volume-title":"Proc. Conference on Functional Programming Languages and Computer Architecture","author":"Turner D. A.","year":"1985"},{"key":"e_1_2_1_3_2","unstructured":"P. W. M.Koopman \u2018Functional programs as executable specifications\u2019 Ph. D. Thesis University of Nijmegen The Netherlands 1990."},{"key":"e_1_2_1_4_2","first-page":"364","volume-title":"Concurrent Clean\u2014a language for functional graph rewriting","author":"Brus T.","year":"1987"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17945-3_9"},{"key":"e_1_2_1_6_2","isbn-type":"print","volume-title":"Functional Programming and Parallel Graph Rewriting","author":"Plasmeijer M. J.","year":"1993","ISBN":"http:\/\/id.crossref.org\/isbn\/0201416638"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54152-7_66"},{"key":"e_1_2_1_8_2","volume-title":"Structured Computer Organization","author":"Tanenbaum A. S.","year":"1984"},{"key":"e_1_2_1_9_2","volume-title":"Studies in logic and foundations of mathematics","author":"Barendregt H. P.","year":"1984"},{"key":"e_1_2_1_10_2","volume-title":"Denotational Semantics, a Methodology for Language Development","author":"Schmidt D. A.","year":"1986"},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-6228-2"},{"key":"e_1_2_1_12_2","volume-title":"The Z notation: A Reference Manual","author":"Spivey J. M.","year":"1989"},{"key":"e_1_2_1_13_2","unstructured":"P. W. M.KoopmanandE. G. J. M. H.N\u00d6Cker \u2018Compiling functional languages to term graph rewrite systems\u2019.Internal Report 88\u20131 Department of Computer Science University of Nijmegen The Netherlands 1988."},{"key":"e_1_2_1_14_2","doi-asserted-by":"crossref","unstructured":"T.Johnsson \u2018Efficient compilation of lazy evaluation\u2019 Proc. ACM SIGPLAN \u203284 Symposium on Compiler Construction 1984 pp.58\u201369.","DOI":"10.1145\/502949.502880"},{"key":"e_1_2_1_15_2","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones S. L.","year":"1987"},{"key":"e_1_2_1_16_2","unstructured":"M. C. J. D.Van Eekelen \u2018Parallel graph rewriting some contributions to its theory its implementation and its application\u2019 Ph. D. Thesis University of Nijmegen The Netherlands 1988."},{"key":"e_1_2_1_17_2","first-page":"317","volume-title":"Term Graph Rewriting, Theory and Practice","author":"Koopman P. W. M.","year":"1993"},{"key":"e_1_2_1_18_2","unstructured":"J. W.Klop \u2018Term rewriting systems: a tutorial\u2019 Note CS\u2010N8701 Centre for Mathematics and Computer Science CWI Amsterdam The Netherlands 1987."},{"key":"e_1_2_1_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_20_2","first-page":"217","volume-title":"Proc. 6th Int. Conf. on Programming","author":"Mycroft A.","year":"1984"},{"key":"e_1_2_1_21_2","unstructured":"J. E. W.Smetsers \u2018Compiling concurrent clean to abstract ABC\u2010machine code\u2019 Technical Report 89\u201320 Department of Computer Sceince University of Nijmegen The Netherlands 1989."},{"key":"e_1_2_1_22_2","unstructured":"G. A.Weijers \u2018ABC\u2010machine implementation guide\u2019 Technical Report University of Nijmegen1990."},{"key":"e_1_2_1_23_2","unstructured":"E. G. J. M. H.N\u00d6Cker \u2018The PABC simulator v0.5. implementation manual\u2019 Technical Report No. 89\u201319 Department of Informatics University of Nijmegen The Netherlands. October1989."},{"key":"e_1_2_1_24_2","unstructured":"J. C.Van Groningen \u2018Implementing the ABC\u2010machine on MC680X0 based architectures\u2019 M. Sc. Thesis University of Nijmegen November1990."},{"key":"e_1_2_1_25_2","volume-title":"Proc. International Conf. for Functional Prog. Languages and Comp. Architectures (FPCA \u203293)","author":"Hartel P. H.","year":"1993"},{"key":"e_1_2_1_26_2","unstructured":"P. W. M.Koopman L. P. J.GroenewegenandG.Engels \u2018Functional description of parallel processes\u2019 Proc. CSN \u203292 Computer Science in the Netherlands SION 1992."}],"container-title":["Software: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fspe.4380250502","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/spe.4380250502","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,25]],"date-time":"2023-10-25T23:45:44Z","timestamp":1698277544000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/spe.4380250502"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,5]]},"references-count":25,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1995,5]]}},"alternative-id":["10.1002\/spe.4380250502"],"URL":"https:\/\/doi.org\/10.1002\/spe.4380250502","archive":["Portico"],"relation":{},"ISSN":["0038-0644","1097-024X"],"issn-type":[{"value":"0038-0644","type":"print"},{"value":"1097-024X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,5]]}}}