Observations and Questions Concerning Partiality and Don't Care Non-Strictness

versus concrete models of specifications Don Sannella Laboratory for Foundations of Computer Science Edinburgh University Edinburgh EH9 3JZ, Scotland dts@dcs.ed.ac.uk In the theory of algebraic specifications, many-sorted algebras are used to model programs: the representation of values is arbitrary and operations are modelled as ordinary functions. The theory that underlies the formal development of programs from specifications takes advantage of the many useful properties that these models enjoy. The models that underlie the semantics of concrete programming languages are di#erent. For example, the semantics of Standard ML uses rather concrete models, where values are represented as closed constructor terms and functions are represented as "closures". The properties of these models are quite di#erent from those of many-sorted algebras. This discrepancy brings into question the applicability of the theory of specification and formal program development in the context of a concrete ..