Operational Semantics Oriented Specification

摘要

The main idea of an Operational Semantics Oriented Specification is to specify algorithms instead of functions. Here, the term represents a state of a calculation as well as a data-object. A confluent transition relation on terms describes the behaviour of the computation. Such a transition relation may be the model of a specification. Weak and strong models are distinguished where the strong models take the sequence of the specification rules into consideration. By a combination of rewriting, with a special form of narrowing, a prototype of models is given which allows the carrying out of specifications. It is shown how confluence in hierarchical specifications can be guaranteed also for nonterminating transition relations.