Logic has proved essential for formally modeling software based systems. Such
formal descriptions, frequently called specifications, have served not only as
requirements documentation and formalisation, but also for providing the
mathematical foundations for their analysis and the development of automated
reasoning tools.
Logic is usually studied in terms of its two inherent aspects: syntax and
semantics. The relevance of the latter resides in the fact that producing
logical descriptions of real-world phenomena, requires people to agree on how
such descriptions are to be interpreted and understood by human beings, so that
systems can be built with confidence in accordance with their specification. On
the more practical side, the metalogical relation between syntax and semantics,
determines important aspects of the conclusions one can draw from the
application of certain analysis techniques, like model checking.
Abstract model theory (i.e., the mathematical perspective on semantics of
logical languages) is of little practical value to software engineering
endeavours. From our point of view, values (those that can be assigned to
constants and variables) should not be just points in a platonic domain of
interpretation, but elements that can be named by means of terms over the
signature of the specification. In a nutshell, we are not interested in
properties that require any semantic information not representable using the
available syntax.
In this paper we present a framework supporting the proof theoretical
formalisation of classes of relational models for behavioural logical
languages, whose domains of discourse are guaranteed to be formed exclusively
by nameable values.