Behavioural Semantics of Algebraic Specifications in Arbitrary Logical Systems

摘要

Behavioural semantics for specifications plays a crucial role in the formalization of the developments process, where a specification need not to be implemented exactly but only so that the required system behaviour is achieved. There are two main approaches to the definition of behavioural semantics: the internal one (called behavioural semantics) and external one (called abstractor semantics). In this paper we present a notion of a behavioural concrete institution which is based on a notion of a concrete institution. The basic idea to form a behavioural institution (i.e. to ensure the satisfaction condition holds) is adopted from [2]. The behavioural concrete institution is a generalization of the COL-institution. In this work we also compare the resulted behavioural semantics with the abstractor semantics.