{"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":1694623910682},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"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,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Some specification languages, such as VDM-SL, allow expressions whose values are not fully determined. This may be convenient in cases where the choice of value should be left to a later stage of development.<\/jats:p>\n          <jats:p>We consider a simple functional language including such under-determined expressions and present a denotational semantics for the language along with a set of proof rules for reasoning about properties of under-determined expressions. One of the specific problems considered is the combination of under-determinedness and a least fixed point semantics of recursion. Soundness of the proof rules is also discussed.<\/jats:p>","DOI":"10.1007\/bf01211050","type":"journal-article","created":{"date-parts":[[2005,2,24]],"date-time":"2005-02-24T15:59:02Z","timestamp":1109260742000},"page":"47-66","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Semantics of under-determined expressions"],"prefix":"10.1145","volume":"8","author":[{"given":"Peter Gorm","family":"Larsen","sequence":"first","affiliation":[{"name":"IFAD, The Institute of Applied Computer Science, Forskerparken 10, DK-5230, Odense M, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo Stig","family":"Hansen","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Technical University of Denmark, Lyngby, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01887198"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bicarregui J. Fitzgerald J.S. Lindsay P. Moore R. and Ritchie B.: Proof in VDM: A Practitioner's Guide. Springer-Verlag 1994.","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Broy M.: A fixed point approach to applicative multiprogramming. In M. Broy and G. Schmidt editors Theoretical Foundations of Programming Methodology pages 565\u2013622. Reidel 1982.","DOI":"10.1007\/978-94-009-7893-5_16"},{"key":"e_1_2_1_2_4_2","unstructured":"British Standards Institution. Z base standard November 1992. Version 1.0."},{"key":"e_1_2_1_2_5_2","unstructured":"The RAISE Language Group.: The RAISE Specification Language . Prentice-Hall 1992."},{"key":"e_1_2_1_2_6_2","unstructured":"Hoare C.A.R.: Communication Sequential Processes . Prentice-Hall 1985."},{"key":"e_1_2_1_2_7_2","unstructured":"Information Technology Programming Languages \u2014 VDM-SL. ISO\/IEC JTC1\/SC22\/WG19 N-20 November 1993. CD 13817-1."},{"key":"e_1_2_1_2_8_2","unstructured":"Jones C.B.: Systematic Software Development Using VDM . Prentice-Hall 1990."},{"key":"e_1_2_1_2_9_2","first-page":"118","volume-title":"Towards Proof Rules for Looseness in Explicit Definitions from VDM-SL","author":"Larsen P.G.","year":"1994"},{"key":"e_1_2_1_2_10_2","unstructured":"Larsen P.G.: Towards Proof Rules for the Full Standard VDM Specification Language. Ph.D. thesis Department of Computer Science Technical University of Denmark March 1995. Technical Report ID-TR: 1995\u2013160."},{"key":"e_1_2_1_2_11_2","volume-title":"Mathematical Logic and Hubert's \u03b5-Symbol","author":"Leisenring A.C.","year":"1969"},{"key":"e_1_2_1_2_12_2","unstructured":"Larsen P.G. and Hansen B.S.: Semantics for Under-determined Expressions. Technical Report ID-TR: 1994-151 Department of Computer Science Technical University of Denmark December 1994."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263649"},{"key":"e_1_2_1_2_14_2","unstructured":"Schmidt D.A.: Denotational Semantics \u2014 A Methodology for Language Development . Allyn and Bacon Inc. 1986."},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.5555\/79245.79247"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/35.5.514"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Tarlecki A. and Wieth M.: A Naive Domain Universe for VDM. In Dines Bj\u00f8rner C.A.R. Hoare and Hans Langmaack editors VDM '90 VDM and Z \u2014 Formal Methods in Software Development pages 552\u2013579. Springer-Verlag 1990.","DOI":"10.1007\/3-540-52513-0_27"},{"key":"e_1_2_1_2_18_2","unstructured":"Walicki M.: Algebraic Specifications of Nondeterminism. Ph.D. thesis University of Bergen Department of Informatics 1993."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01211050.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211050\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211050","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:23:40Z","timestamp":1641482620000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211050"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,1]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1996,1]]}},"alternative-id":["10.1007\/BF01211050"],"URL":"https:\/\/doi.org\/10.1007\/bf01211050","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,1]]}}}