Transforming Specifications of Observable Behaviour into Programs

A methodology for deriving programs from specifications of observable behaviour is described. The class of processes to which this methodology is applicable includes those whose state changes are fully definable by labelled transition systems, for example communicating processes without internal state changes. A logic program representation of such labelled transition systems is proposed, interpreters based on path searching techniques are defined, and the use of partial evaluation techniques to derive the executable programs is described. 1 Motivations Our methodology provides a means for deriving executable programs from specifications of the observable behaviour of a restricted class of systems. The systems which are tractable by this methodology are those whose observations are discrete fine-grained steps which progressively construct data objects, expressed as terms in our approach. We give the characterisation of these systems by the use of a language based on labelled transitio..