Semantics of under-determined expressions

Abstract

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.