We introduce a framework that generalizes algebraic specifications by equipping algebras with descriptions of evaluation strategies. The resulting abstract mathematical description allows one to model the implementation of algebras on various platforms in a way that is independent of the function-oriented specifications. We study algebras with associated data dependencies. The latter provide separate means for modelling computational aspects apart from the functional specifications captured by an algebra. The formalization of evaluation strategies (1) introduces increased portability among different hardware platforms, and (2) allows a potential increase in execution efficiency, since a chosen evaluation strategy may be tailored to a particular platform. We present the development process where algebraic specifications are equipped with data dependencies, the latter are refined, and, finally, mapped to actual hardware architectures.

The article defines algebraic semantics of singular (call-time-choice) and plural (run-time-choice) nondeterministic parameter passing and presents a specification language in which operations with both kinds of parameters can be defined simultaneously. Sound and complete calculi for both semantics are introduced. We study the relations between the two semantics and point out that axioms for operations with plural arguments may be considered as axiom schemata for operations with singular arguments.

The current algebraic models for nondeterminism focus on the notion of possibility rather than necessity and consequently equate (nondeterministic) terms that one would intuitively not consider equal. Furthermore, existing models for nondeterminism depart radically from the standard models for (equational) specifications of deterministic operators. One would prefer that a specification language for nondeterministic operators be based on an extension of the standard model concepts, preferably in such a way that the reasoning system for (possibly nondeterministic) operators becomes the standard equational one whenever restricted to the deterministic operators—the objective should be to minimize the departure from the standard frameworks. In this article we define a specification language for nondeterministic operators and multialgebraic semantics. The first complete reasoning system for such specifications is introduced. We also define a transformation of specifications of nondeterministic operators into derived specifications of deterministic ones, obtaining a “computational” semantics of nondeterministic specification by adopting the standard semantics of the derived specification as the semantics of the original one. This semantics turns out to be a refinement of multialgebra semantics. The calculus is shown to be sound and complete also with respect to the new semantics.

An object-oriented approach to formal specification of reactive systems is described. The main contributions of the work are: a language for specifying and implementing reactive modules; inheritance operations for such specifications and implementations; a formal semantics for such reactive programs and for the inheritance operations in terms of partial orders of events; treatment of specifications as types of modules and treatment of modules as first-class objects; and discussion of subtyping among specifications.>

In distributed systems it is often important to be able to determine the temporal relationships between events generated by differentprocesses.An algorithm

We describe a general module language integrating abstract data types, specifications and object-oriented concepts. The framework is based on the Standard ML module system, with three main extensions: subtyping, a form of object derived from ML structures, and inheritance primitives. The language aims at supporting a range of programming styles, including mixtures of object-oriented programming and programs built around specified algebraic or higher-order abstract data types. We separate specification from implementation, and provide independent inheritance mechanisms for each. In order to support binary operations on objects within this framework, we introduce "internal interfaces" which govern the way that function components of one structure may access components of another. The language design has been tested by writing a number of program examples; an implementation is under development in the context of a larger project. 1 Introduction This paper describes a general module sys...