{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:51:50Z","timestamp":1694623910371},"reference-count":11,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[1996,9,1]],"date-time":"1996-09-01T00:00:00Z","timestamp":841536000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1996,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The formal specification language Z is strongly typed, but has a rather inexpressive type system in which essentially the only type constructors are power set and Cartesian product. This paper explores the possibility of using a richer type system for extracting information about a Z specification, so that properties like being a function or a sequence become part of the type of an expression. This richer type system adds further type constructors to the sparse set contained in the language definition, and uses properties of Z's library functions to infer information about complex expressions from information about their simpler parts.<\/jats:p>","DOI":"10.1007\/bf01211909","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T19:28:44Z","timestamp":1109359724000},"page":"565-584","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Richer types for Z"],"prefix":"10.1145","volume":"8","author":[{"given":"Michael","family":"Spivey","sequence":"first","affiliation":[{"name":"Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Boyer R. and Moore J. S.: A computational logic . Academic Press 1979."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Cardelli L.: \u2018A Semantics of Multiple Inheritance\u2019 in Semantics of Data Types (G. Kahn D. B. MacQueen and G. Plotkin eds.) LNCS 173 Springer-Verlag 1985","DOI":"10.1007\/3-540-13346-1_2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Dershowitz N.: \u2018Orderings for term-rewriting systems\u2019 Theoretical Computer Science March 1982.","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_2_1_2_5_2","unstructured":"Mitchell J. C: \u2018Polymorphic type inference and containment\u2019 in Logical foundations of functional programming (G. Huet ed.) Addison-Wesley 1990."},{"key":"e_1_2_1_2_6_2","unstructured":"Nicholls J. E. (ed.): Draft Z standard Oxford University Computing Laboratory 1995."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_2_8_2","unstructured":"Spivey J. M.: Understanding Z: a specification language and its formal semantics Cambridge University Press March 1988."},{"key":"e_1_2_1_2_9_2","unstructured":"Spivey J. M.: The Z notation: a reference manual Prentice-Hall International November 1989. Second edition March 1992."},{"key":"e_1_2_1_2_10_2","unstructured":"Spivey J. M.: The fuzz manual The Spivey Partnership 1992."},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Spivey J. M. and Sufrin B. A.: \u2018Type inference in Z\u2019 in VDM and Z \u2014 Formal methods in software development (D. Bj\u00f8rner C. A. R. Hoare and H. Langmaack eds.) LNCS 428 Springer-Verlag April 1990.","DOI":"10.1007\/3-540-52513-0_22"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211909.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211909\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211909","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:28:17Z","timestamp":1641482897000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211909"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,9]]},"references-count":11,"journal-issue":{"issue":"5","published-print":{"date-parts":[[1996,9]]}},"alternative-id":["10.1007\/BF01211909"],"URL":"https:\/\/doi.org\/10.1007\/bf01211909","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,9]]}}}