Semantics of under-determined expressions
- 1 January 1996
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 8 (1) , 47-66
- https://doi.org/10.1007/bf01211050
Abstract
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. 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.Keywords
This publication has 8 references indexed in Scilit:
- Towards Proof Rules for Looseness in Explicit Definitions from VDM-SLPublished by Springer Nature ,1994
- Proof in VDM: A Practitioner’s GuidePublished by Springer Nature ,1994
- Non-determinism in Functional LanguagesThe Computer Journal, 1992
- Referential transparency, definiteness and unfoldabilityActa Informatica, 1990
- A naive domain universe for VDMPublished by Springer Nature ,1990
- Do-it-yourself type theoryFormal Aspects of Computing, 1989
- Non-deterministic data types: models and implementationsActa Informatica, 1986
- A Fixed Point Approach to Applicative MultiprogrammingPublished by Springer Nature ,1982