The Computer Journal Advance Access originally published online on August 22, 2007
The Computer Journal 2008 51(2):181-191; doi:10.1093/comjnl/bxm031
| ||||||||||||||||||||||||||||||||||||||||||||||||||
On the Behavioral Equivalence Between k-data Structures
Department of Mathematics, University of Aveiro, 3810-193 Aveiro, Portugal
* Corresponding author: martins{at}mat.ua.pt
Received 28 February 2006; revised 1 May 2007
Throughout this paper we consider data structures as sorted algebras endowed with a designated subset of their visible part, which represents the set of truth values. The originality of our approach is the application of the standard abstract algebraic logic theory of deductive systems to the hidden heterogeneous case. We generalize the well-known equivalence relation between finite automata, which relies on the Nerode equivalence relation between states, to k-data structures. This is obtained via the Leibniz congruence, which can be viewed as a generalization of the Nerode equivalence in automata theory.
Key Words: data structures • behavioral equivalence • Leibniz congruence • Nerode equivalence • hidden logic
 |
1. INTRODUCTION |
|---|
 TOP 1. INTRODUCTION 2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
In the traditional algebraic approach to the specification of programs, sorted algebras are used to model the programs that manipulate several sorts of data. However, object-oriented (OO) systems constitute a challenge for traditional algebraic methods. They, very often, provide mechanisms to encapsulate internal data in order to make the updating of programs easier and, the internal data protected; the latter can be required by security reasons. Consequently, the data should naturally be split into two categories: the ones to which the user has direct access to (visible data) and those that the user only has access to by the meaning (output) of programs with visible output (hidden data).
In this work, we are interested in the study of a special relation between hidden data elements, called behavioral equivalence relation; intuitively, two hidden data elements are said to be behaviorally equivalent if the output over each program of visible range is the same when we use either element as input (this relation was introduced by Reichel [1]).
Observational techniques are very important in formal methods for verification and specification of programs. Indeed, given a specification, in order to prove the correctness of an abstract machine, we should forget its internal characteristics, since the intrinsic behavior should be examined only via programs with visible output.
Our approach to behavioral equivalence differs substantially from that adopted in most of the previous works in this area in the sense that it is greatly influenced by abstract algebraic logic (AAL). This is, in fact, the main novelty of our work. The AAL is an area of algebraic logic that focuses on the study of the relationship between logical equivalence and logical truth (cf. [2]). The AAL is centered on the process of associating a class of algebras to a logical system. This feature contrasts with the usual treatment given in pure algebraic logic where the emphasis is on the study of the class of algebras obtained by this process.
In order to apply the results and tools of AAL to the theory of specification of abstract data types, we have to look at the specification logic as a deductive system, i.e. as a substitution-invariant closure relation on an appropriate set of formulas. The class of deductive systems has to be expanded in order to include multisorted, as well as one-sorted systems, and to provide for the dichotomy ‘visible versus hidden’. We also have to be able to formulate, in this context, the behavioral equivalence as some generalized notion of the Leibniz congruence.
The notion of deductive system is generalized by considering the data to be heterogeneous and split into two kinds: the visible and the hidden ones. By a k-data structure we mean a collection of data items of different sorts, like lists, Booleans, numbers, etc., and operations involving them, together with a set of k-tuples of elements, as a set of generalized truth values, called a filter. The universe, which is a sorted algebra, is split into two disjoint sets, namely: the hidden part, which corresponds to the states of the associated state transition system and the visible part. There are also two different kinds of interpretation of the operation symbols: the attributes and the methods. The former return visible data and are used for observing the state of the system while the latter may represents changes of state. The k-data structures play an important role in the algebraic specification of OO programs. Namely, they are the natural models of generalized hidden k-logics (cf. [3, 4]). Hidden k-logics are useful mainly because they encompass not only the two-dimensional hidden and standard equational logics, but also the Boolean logics; these are one-dimensional multisorted logics with Boolean as the only visible sort, and with equality-test operations for some of the hidden sorts in place of equality predicates. They also include all assertional logics of the standard AAL.
Concerning the notion of Leibniz congruence, it has to be generalized by considering the distinctive characteristics of the OO paradigm. In [4], the authors proposed a general notion of Leibniz congruence. They showed that the Leibniz congruence coincides with the behavioral equivalence relation; thus, it is worth to explore this notion within the OO paradigm. The Leibniz congruence on an algebra A over a designated filter F, denoted by 
(F), is defined as the largest congruence on A compatible with F. A congruence relation 
on A is compatible with F if for all V 
VIS and for all 
, ' AVk, ai 
a'i (V) for all i 
k, implies that ( FV iff ' FV). A useful property is the fact that the Leibniz congruence is preserved under inverse images of surjective homomorphisms. This allows us to generalize to k-data structures the characterization of the global behavioral equivalence relation between finite automata based on the well-known Nerode equivalence relation on the states of the automaton. Namely, we show that two k-data structures are equivalent (i.e. they have the same behavior) if and only if their quotients, under the respective Leibniz congruences, are isomorphic (Theorem 4.1).
|
2. PRELIMINARIES |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
Let SORT be a nonempty set (the elements in SORT are called sorts). A nonempty finite sequence S0, ... , Sn of sorts in SORT is called a type over SORT. We will write a type as S0, ... , Sn–1
Sn. The set of all types is denoted by TYPE. From the beginning, we distinguish visible and hidden data by splitting, in the definition of signature, the set of sorts in the visible and the hidden part. A hidden (sorted) signature is a triple 
= 
SORT,VIS,OP
, where SORT is a nonempty set of sorts, VIS is a subset of SORT, which we call the set of visible sorts and OP = OP
: TYPE, where OP is a countable set of operation symbols of type . We call the sorts in SORT\VIS hidden sorts. We assume X = XS:S SORT to be a fixed countable sorted set of variables. We define the sorted set Te(X) of terms (or formulas) in the signature as usual. We say that a term t is a ground term (or a variable-free term) if it does not have variables. We say that a hidden signature is standard if there is a ground term of each sort.
2.1. Sorted algebra
By a -algebra (or simply an algebra, if is clear from the context), we mean a pair A = AS : S SORT, OPA : TYPE, where AS is a nonempty set for each S SORT and, for each TYPE ( = S0, ... , Sn–1 Sn), OPA = OA: O OP, where OA is an operation on A of type , that is OA : AS0 x ··· x ASn–1 ASn. Throughout this paper, we assume that AS 
, for all S SORT. With this assumption, we exclude some data structures of practical interest. However, the meta-mathematics is simpler in this case and most results of universal algebra hold in their usual form. More generally, the assumption holds automatically if is standard.
We define, in the usual way, the operations in Te(X) to obtain the term algebra over the signature , which we denote by Te(X). It is well known that Te(X) has the universal mapping property over X in the sense that, for every -algebra A and every sorted map h : X A, called an assignment, there is a unique sorted homomorphism h* : Te(X) A which extends h. In the sequel, we will not distinguish between these two maps. A map from X to the set of terms, and its unique extension to an endomorphism of Te(X), is called a substitution. Since X is assumed fixed throughout the paper, we normally write Te in place of Te(X); moreover, we may write simply Te when is clear from the context.
Example 2.1. (Flags)
The hidden signature of flags,
|
|
Example 2.2. (Sets)
The hidden signatureand
. The hidden operations are the constant empty to represent the empty set; and union, & and neg to represent the set theoretical union, intersection and complement, respectively. The action of adding an element to a set is represented by add and, in is the operation symbol used to test whether an element belongs to a set; i.e., in (e, X) expresses that ‘e is in X’ (cf. Figs. 3 and 4).
|
|
Example 2.3. (Stacks)
The signature of the stacks of natural numbers,
|
|
To provide a context that allows us to deal simultaneously with specification logics that are sentential (for example, logics with a Boolean sort) and equational, we introduce the notion of a k-term for any non-zero natural number k (cf. [3]). A k-term of sort S over
is just a sequence of k -terms, all of the same sort S. We indicate k-terms by overlining, 
: S = 
0 : S, ... , k–1 : S. When we do not want to make the common sort of each term of explicit, we simply write it as . Tek is the sorted set of all k-terms over ; i.e. Tek = TeSk : S SORT. The set of all visible k-terms (Tek)VIS is the set (Tek)V : V VIS. A k-variable is the special k-term 
consisting of k distinct variables x0 : S, ... , xk–1 : S all of them of the same sort.
Recall that for every algebra A over and every assignment h : X A, there is a unique homomorphism h* : Te A which extends h. We also define a map 
* : Tek Ak by *() : =*(0, ... , k–1) : =h*(0), ... , h*(k–1). In the sequel, if it is clear from the context, we will denote all these maps by the same symbol h.
2.2. Data structures
By a k-data structure we mean a collection of data items of different sorts, like lists, booleans, numbers, etc., and operations involving them. Some of the data items are considered hidden in the sense that we do not have direct access to them. In our approach, a k-data structure is endowed with a set of generalized truth values, called a filter (the term filter comes from the one sorted case in the AAL field).
Definition 2.1
A visible k-data structure (or simply a k-data structure) over=
AVISk : =
An example of a two-data structure is any model of the free hidden equational logic over
Example 2.4. (Flags—revisited I)
A two-data structure over
- upA(U) = upA(U') = upA(D) = U;
- dnA(U) = dnA(U') = dnA(D) = D;
- revA(U) = revA(U') = D; revA(D) = U;
- upA?(U) = upA?(U') = true and upA?(D) = false.
We take the usual Boolean operations of the two-element Boolean algebra B2 and the filter the set F = {
Example 2.5. (Sets—revisited)
This is a more interesting example since there are two visible sorts involved. Let Belt be a nonempty set of elements. Then we define Bset
(Belt), the set of all subsets of Belt, and Bbool : ={true, false}.
Let B be the sorted set
- emptyB =
- unionB(C1, C2) = C1
C2; addB(e, C) = {e}
- negB(C) = Belt\C; &B(C1, C2) = C1
C2;
- trueB = true; falseB = false;
- ¬B = ¬;
Let F =
=
2.3. Leibniz congruence
Let A, F be a k-data structure over a hidden signature . A congruence relation on A is VIS-compatible (or simply compatible) with F if for all V VIS and for all , 'AVk ai a'i (V) for all i k, implies that, FV iff ' FV. Equivalently, we have that is compatible with F if and only if for every V VIS, FV is the union of a cartesian product of V-classes. If a congruence is compatible with F, then any congruence that is contained in is also compatible with F. But being compatible with F does not imply that is compatible with any G contained in F. However, if is compatible with each member of a set U of filters then it is compatible with its intersection U. The fact that a congruence is compatible with F also does not imply that it is compatible with any G that contains F. It is not difficult to see that the largest congruence compatible with F always exists (cf. [3]).
Definition 2.2. (Leibniz congruence)
Let
We use the term ‘Leibniz congruence’ since this notion generalizes the analogous concept from the one-sorted case. The Leibniz congruence plays a central role in our research. The term was introduced in [5], but the concept appeared much earlier in the context of AAL. In the one-sorted case it has extensively been investigated (cf. [2, 5]).
Bidoit et al. in [6] consider the algebras as being endowed with a congruence that can be viewed as the Leibniz congruence on the equality models over the identity filter. Goguen and Malcolm in [7] also study this congruence for equality models.
We say that a k-data structure = A, F is reduced if (F) is the identity congruence on A.
Example 2.6. (Nerode Equivalence)
It is well known that any finite automaton can naturally be presented as a multi-algebra. However, Blok and Pigozzi pointed out that they are even more naturally viewed as one-data structures (cf. [8]). Let
Example 2.7. (Flags—revisited II)
Let
Let A be an algebra, (x0 : T0, ... , xn–1 : Tn–1) a k-term and a0 AT0, ... , an–1 ATn–1. Then, we denote by A(a0, ... , an–1) the value that takes in A, when the variables x0, ... , xn–1 are interpreted, respectively, by a0, ... , an–1. More algebraically, A(a0, ... , an–1) = h(), where h : X A is any assignment such that h(xi) = ai for all i < n.
A (visible) k-context over is a (visible) k-term (z : S, x0 : T0, ... , xm–1 : Tm–1) : V Tek(X), with a distinguished variable z of sort S and parametric variables x0, ... , xm–1.
A systematic study of the properties of the Leibniz congruence in hidden k-logics can be found in [3]; in particular a proof of the following characterization of the Leibniz congruence can be found there.
Theorem 2.1. [4]
Let
In two-data structures, the filters are themselves sets of pairs, so a strict relationship between them and their Leibniz congruence can be established (cf. [3]). As an example we have the following proposition.
Proposition 2.1
Let
F
- If F is reflexive (on AVIS) and transitive then
Let A be an algebra and C A2. The congruence generated by C in A is the smallest congruence on A that contains C; it will be denoted by 
(C).
Given a two-data structure = A, F with F reflexive (on AVIS) and transitive, if (F {a, a'})VIS = F, then, from (2) of Proposition 2.1, (F {a, a'}) is compatible with F. Hence, (F {a, a'}) (F). Therefore, a a' ((F)).
|
3. HOMOMORPHISMS AND PRODUCTS |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
Let
be a hidden signature and, = A, F and = B, G be k-data structures over . We say that is a k-data substructure of , in symbols , if A is a subalgebra of B and G AVISk = F. Let h be a sorted homomorphism from the algebra A into the algebra B; we say that h is a data structure homomorphism from to if h(F)G, or equivalently, if Fh–1(G), and we denote it by h : . If F = h–1(G), then h is said to be strict. We say that h is surjective if it is surjective as a sorted map and we write h : 
; h is said to be injective if it is injective as a sorted map and h(F) = G h(Ak), i.e. h–1(G) = F, and we write h : . We say that h is a data structure isomorphism if it is injective and surjective, i.e. h is an algebra isomorphism and h(F) = G. In this case, we write 
.
We define the direct product of the family (i)iI of k-data structures to be the k-data structure 
iI i = iI Ai,iIFi, where iIAi is the direct product of the family of algebras (Ai)iI and iIFi = iI (Fi)V : V VIS. The index set I may be empty; in this case iIAi is the trivial one-element algebra. A k-data substructure of iIi is called a subdirect product of the family (i)iI, in symbols SD iIi, if the homomorphism projection 
i : B Ai is surjective for every i I.
One of the main properties of the Leibniz congruence is its preservation under inverse images of surjective homomorphisms.
Lemma 3.1. [4]
Let
If = A, F is a k-data structure over and is a congruence on A compatible with F, then we can consider the quotient of by , / : =A/, FV/V : V VIS, where FV/V = {a0/V, ... , ak–1/V : a0, ... , ak–1 FV}. We should note that the compatibility condition means that a0/V, ... , ak–1/V FV/V if and only if a0, ... , ak–1 FV. If = (G) for some filter GAVISk, then we can simply write /G = A/(G), F/(G). The special case when is (F), the quotient /F is called the reduction of and it is denoted by *. Bidoit et al. call the reduction of the black box view of (cf. [6]). It was proved in [4] that the quotient of any k-data structure by the Leibniz congruence is always reduced. It is also easy to see that the natural homomorphism h : A A/(F) is a data structure homomorphism. In fact, it is a strict homomorphism. Hence, if is itself reduced then *.
The following theorem states that the natural generalization of the homomorphism theorem holds for k-data structures.
Theorem 3.1. (Homomorphism theorem)
Let
Proof
Since h is strict, F = h–1(G). ThusB) = ker(h); the third equality holds because
Then by the homomorphism theorem for sorted algebras h* : A/
A more general version of this theorem can be formulated. It applies to arbitrary k-data structures: if and are possibly non reduced k-data structures and h : is a surjective data structure morphism, then /h–1(G) *. This result can be shown as a corollary of Theorem 3.1 and it points out the importance of being reduced in the hypothesis of the theorem.
The Birkhoff's subdirect representation also holds when restricted to the class of reduced k-data structures. The proof is similar to that of the one sorted case (cf. [8]).
Theorem 3.2
A reduced k-data structure
i
Proof
Suppose thatSince the projection homomorphisms are surjective and each
To prove the reciprocal, suppose that there are Fi, i
Then h is a subdirect embedding of A in
|
4. GLOBAL BEHAVIORAL EQUIVALENCE |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
In this section, we consider a relation on the class of k-data structures upon which lies the general idea of behavioral equivalence between k-data structures described in Section 1. We will call such a relation global behavioral equivalence. Actually, this relation generalizes the notion of automata equivalence in automata theory (cf. [9, 10]). We show that two k-data structures are behaviorally equivalent if and only if their reductions (the quotients by their Leibniz congruence relations) are isomorphic (cf. Theorem 4.1).
Definition 4.1. [11]
Let: Y
|
|
It is straightforward to show that the global behavioral equivalence between k-data structures is an equivalence relation on the class of all k-data structures over . If beh, we sometimes say that and have the same ‘behavior’.
Given two globally behaviorally equivalent k-data structures = A, F and = B, G, we can define a relation between their universes (which is usually called bisimulation) in the following way. Let :Y A and : Y B be the mappings that witness the equivalence between and . Then the bisimulation relation between and is the relation R A x B defined by RS = {(y),(y) : y YS}.
Just as the Leibniz congruence can be viewed as a generalization of the relation of Nerode equivalence in automata theory (Example 2.6), the global behavioral equivalence of k-data structures may be seen as a generalization of the equivalence of finite-state machines.
The following theorem generalizes the characterization of equivalence between finite automata. It states that two k-data structures have the same behavior if and only if their quotients, under the respective Leibniz congruences, are isomorphic.
Similar results have been established in the context of hidden equational logics and observational logics (cf. Hennicker [12] and, Hofmann and Sannella [11]). Our result is more general since it applies to any hidden k-logic.
Theorem 4.1
Two k-data structures
Proof
AssumeWe claim that:
Claim
There is an algebra epimorphism from A onto B/G.
In fact, let us define h : A B/G by
|
|
(t). Such t always exists since is surjective.
First we prove that the map h is well defined. That is, if t and t' are such that a = (t) = (t'), then (t)/(G) = (t')/(G). Let t and t' be terms such that
|
| (1) |
We have that the congruence generated by (–1((F))) is compatible with G. Indeed, since is surjective, is the transitive closure of (–1((F))). Hence, it is enough to prove that (–1((F))) is compatible with G because if this is the case, obviously the transitive closure is also compatible with G.
Suppose that G and 
((–1((F))k). Then there are i, 
iTe(Y) such that ai = (i), bi= (i), i < k and 
(–1((F))k). Then,
|
| (2) |
= () is in G, () F. Therefore, by compatibility, equation (2) implies () F. And, again by the definition of behavioral equivalence we have that = () G.
From equation (1), we have that (t) (t') (). In fact, since (t) = (t'), t t'(–1((F))). Hence, (t) (t')((–1((F)))). Thus, since (–1((F))) is compatible with G, (t) (t') ((G)).
It is easy to see that h is surjective, because is surjective. To prove that h is an algebra homomorphism let O be an operation symbol in of type S0,... , Sn–1 Sn and a0,... ,an–1 AS0 x ···x ASn–1. For each i < n, there is a term ti such that h(ai)= (ti)/(G) with (ti) = ai.
On the other hand,
|
|
|
|
|
|
Let 
F. Then h() = ()/(G), where fi = (i) i < k (note that, for every Ak and any congruence , / denotes a0/, ... ,ak–1/). So () G, by hypothesis. Hence, h(F) G/(G). That is, h is a data structure homomorphism.
Let now 
G/(G). Hence, = 
/(G) for some G. Since is surjective, for each i < k there is a i such that (i) = gi. Let (0), ... , (k–1). We have that F, because (0), ... ,(k–1) = G. Moreover, h(fi) = (i)/(G) =gi/(G). Thus, h() = /(G). Therefore, h–1(G/(G)) = F. That is, h is strict.
Since /G is reduced, by the Homomorphism Theorem, we have that /F is isomorphic to /G.
To prove the reciprocal implication in the theorem, assume /F /G. Let i : /F /G be a data structure isomorphism. Suppose that A and B are disjoint (if not, replace them by disjoint isomorphic copies). Take Y to be the set of variables defined by Y = {ya:a A} {yb:b B}.
For each b B, we choose ab A such that i(ab/(F)) = b/(G) and for each a A we choose ba B such that i(a/(F)) = ba/(G).
Define assignments and in the following way:
- : Y A by
- :Y B by
By definition of isomorphism, we have
|
|
On the other hand, it can be proven, by induction, that for every Te(Y),
|
| (3) |
Now we are going to prove that () F 
() G. Let () F. Then ()/(F) F/(F). Hence, i(()/(F)) i(F/(F)). Since i is a data structure isomorphism, i(()/(F)) G/(G).
By equation (3), ()/(G) G/(G). That is, () g((G)k), for some g G. Therefore, by compatibility, () G.
Let () G. Then ()/(G) G/(G). Hence, i–1(()/(G)) F/(F). By equation (3), ()/(F) F/(F). So, there exists f F such that () f ((F)k). By compatibility, () F.
In the literature, e.g. [11], an equivalence relation on the class of all k-data structures over a fixed signature such that for all k-data structures and , implies * *, is called behaviorally factorizable.
|
5. HIDDEN LOGIC |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
As it is usually adopted in sentential logic frameworks, we will refer to k-formulas as a synonymous of k-terms. A finite k-sequent is a finite sequence of k-formulas
0:S0, ... ,n–1: Sn–1,n:Sn that we write in the following form:
|
| (4) |
0,... ,n in the k-sequent are visible k-formulas, then we call it a visible k-sequent.
The set F of a given k-data structure = A, F is understood to represent the set of ‘truth values’ of . With this meaning in mind, the following definitions of some semantic concepts will seem more natural.
A visible k-formula :V is said to be a semantic consequence in of a set of visible k-formulas 
, in symbols 
, if, for every assignment h:X A, h() FV whenever h() FW for every :W . A visible k-formula is a valid k-formula, or simply a validity, of , and conversely is a model (or a correct abstract machine) of , if . A visible k-sequent such as equation (4) is a valid rule, or simply a validity, of , and conversely is a model of the k-sequent, if {0,... ,n–1} n.
A visible k-formula is a semantic consequence of in an arbitrary class K of k-data structures over , in symbols K , if for each K. Similarly, a k-formula or rule is a validity of K if it is a validity of each member of K.
In our approach, the underlying logics used to specify computational systems, which we call hidden k-logics, have been defined as abstract closure relations on the set of visible k-formulas (cf. [4]). Specifically, a hidden k-logic is a pair 
= ,
, where is a hidden signature and is a substitution-invariant closure relation on the set of visible k-formulas, called the consequence relation of . This consequence relation may be finitary or not. It is said to be finitary just in case it admits a presentation by axioms and inference rules, in the usual Hilbert style. In this case, is said to be specifiable. An -theory of a hidden k-logic is a set of visible k-formulas that are closed under the consequence relation . The set of all -theories is denoted by Th(); it forms an lattice under set inclusion. An important hidden two-logic is the hidden equational logic, where it is considered only a primitive notion of equality between visible data. It is defined by the reflexivity, symmetry, transitivity and congruence rules, as a sorted equational logic, but only on the visible part (cf. [4]).
The following proposition states that for any class K of k-data structures K is always a hidden k-logic.
Proposition 5.1
Let K be a class of k-data structures, all of them over the same hidden signature
Proof
The proof that
is a model of a hidden k-logic if every consequence of is a semantic consequence of ; i.e. implies . The class of all models of is denoted by Mod(). If is a specifiable hidden k-logic, presented by a set of axioms and rules of inference, then is a model of if and only if every axiom and every rule of inference of is a validity of . The Completeness theorem holds for hidden k-logics, i.e. for any hidden k-logic and every {}(Tek)VIS, iff Mod() (cf. [3]).
A k-data structure = A, F is a behavioral model of (reduced model in the AAL sense) if it is reduced and a model of . The class of all behavioral models is denoted by Mod*(). Bidoit et al. call this class of models, in the context of observational logics, black box semantics (cf. [6]). In [13], the author presents an exhaustive study of the class of behavioral models by relating closure properties with classifications of the axiomatization it admites.
Example 5.1. (Stacks—revisited I)
The standard algebra of stacks of natural numbers is the following sorted algebra.
Snat=
, Sstack = {
Note that pushS(
The two-data structure
=
Proposition 5.2
Let
- For each
- For all
Proof
- Assume h(
- Assume
)
As a consequence of this theorem we have that
Corollary 5.1
Let
Proof
This is an immediate consequence of the fact that under the assumption that
From this corollary, we can easily conclude that Mod() is closed under behavioral equivalence beh.
|
6. CONCLUSIONS AND RELATED WORK |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
This generalization of the AAL theory, which allows the introduction of multisorts and accommodates the dichotomy ‘visible versus hidden’, is relevant in its own right. Moreover, it is recognized that its application to the OO paradigm has been very successful; several results have been obtained using AAL methods (cf. [3, 4, 13, 14]). Furthermore, this new bridge between the AAL and the specification and verification theory of programs has an enormous potencial for new developments.
Hidden k-logics, as a natural generalization of deductive systems, were introduced by Martins and Pigozzi [4]. The theory was developed in [3], where the improvements concerning specification and verification of programs were established using tools from AAL. The theory of hidden k-logics provides a unified treatment for several logical systems such as assertional logics, Boolean logics (one-dimensional multisorted logics with Boolean as the only visible sort, and with equality-test operations for some of the hidden sorts in place of equality predicates), equational and inequational logics and the corresponding hidden versions of all of these.
A similar notion to our concept of bisimulation, called homomorphism relation, was used by Leavens and Pigozzi to study the behavioral subtyping in models of hidden equational logic having the same visible part and with filters being the identity relation on the visible part; i.e. over fixed data semantics (cf. [15, 16]). This relation has also been studied in other contexts: (1) Casanovas et al. examined in [17] this relation in the context of equality-free logics. They called the relation by relativeness correspondence. (2) Malcolm studied bisimulation in the coalgebra field (e.g. [18]). He assumed that the visible part is fixed at the signature level and that there are restrictions with respect to the operation symbols in order to be able to deal with models as coalgebras; namely, the methods have to have at most one hidden argument. (3) Hofmann and Sannella presented in [11] a similar result to our Theorem 4.1 but they dealt exclusively with the hidden equational case, i.e. they analyzed the bisimulation relation for ordinary two-data structures.
All of these approaches, as well as ours, may be seen as a generalization of Schoett's technique (cf. [19]). He argued that an algebra A may be used in place of another algebra B without exhibiting surprising behavior, if the two algebras are behaviorally equivalent in the sense that any program that is run in both the two algebras yields the same output. He made the additional assumption that only visible data can be legitimate output of programs. Moreover, he proved that the existence of a bisimulation between A and B is both necessary and sufficient for A being behaviorally equivalent to B.
Our results differ from the ones listed above since they hold for any hidden k-logic, while the previous results are restricted to observational logic, or to hidden equational logic or to equality-free logics. Moreover, our k-data structures are endowed with a set of truth values in order to be part of hidden k-logic semantics. Behavioral equivalence appears as the largest congruence compatible with the set of truth values in opposition to the other cases where behavioral equivalence is part of the data structure. Actually, this approach seems to us to be the most appropriate way to deal with OO systems: the k-data structures should be viewed as abstract machines satisfying some visible properties (expressed by axioms) and whose behavior is elicited by testing the behavior of the abstract machine under the ‘experiments’.
|
ACKNOWLEDGEMENTS |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
The author would like to thank the referees for their comments that improved the quality of this paper and, Don Pigozzi and Isabel Ferreirim for some fruitful discussions concerning this work.
|
NOTES |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
This research was supported by Fundação para a Ciência e a Tecnologia (Portugal) through Unidade de Investigação Matemática e Aplicações of University of Aveiro.
|
REFERENCES |
|---|
|
TOP1. INTRODUCTION2. PRELIMINARIES3. HOMOMORPHISMS AND PRODUCTS4. GLOBAL BEHAVIORAL EQUIVALENCE5. HIDDEN LOGIC6. CONCLUSIONS AND RELATED...ACKNOWLEDGEMENTSNOTESREFERENCES |
|---|
-
[1] Reichel H. Behavioural validity of conditional equations in abstract data types. (1985) Contributions to general algebra 3. Proc. Conf., Vienna 1984, June. Teubner, Stuttgart: Verlag B.G. 301–324.
[2] Pigozzi D. Abstract algebraic logic. In: Encyclopedia of Mathematics, Supplement III—Hazewinkel M., ed. (2001) Dordrecht: Kluwer Academic Publishers. 2–13.
[3] Martins M. Behavioral reasoning in generalized hidden logics. In: PhD Thesis (2004) University of Lisbon, Faculdade de Ciências.
[4] Martins M., Pigozzi D. Behavioural reasoning for conditional equations. In: Math. Struct. in Comp. Science (2007) 17(5):1075–1113.
[5] Blok W., Pigozzi D. Algebraizable logics. Mem. Am. Math. Soc. (1989) 77(396).
[6] Bidoit M., Hennicker R., Wirsing M. Behavioural and abstractor specifications. Sci. Comput. Program. (1995) 25:149–186.[CrossRef]
[7] Goguen J., Malcolm G. A hidden agenda. Theor. Comput. Sci. (2000) 245:55–101.[CrossRef]
[8] Blok W., Pigozzi D. Algebraic semantics for universal Horn logic without equality. In: Res. Expo. Math—Romanowska A., Smith J.D.H., eds. (1992) 19. Universal algebra and quasigroup theory, Lect. Conf, 1989. Berlin: Heldermann Verlag. 1–56.
[9] Denecke K., Wismath S. Universal Algebra and Applications in Theoretical Computer Science. (2002) Boca Raton, FL: Chapman and Hall/CRC.
[10] Hopcroft J., Ullman J., Motwani R. Introduction to Automata Theory, Languages, and Computation (2001) 2nd ed. Reading, MA: Addison-Wesley.
[11] Hofmann M., Sannella D. On behavioural abstraction and behavioural satisfaction in higher-order logic. Theor. Comput. Sci. (1996) 167:3–45.[CrossRef]
[12] Hennicker R. Structural Specifications with Behavioural Operators: Semantics, Proof Methods and Applications (1997) Habilitationsschrift. Institut für Informatik, Ludwig-Maximilians-Universität München.
[13] Martins M. Closure properties for the class of behavioral models. Theor. Comput. Sci. (2007) 379(1–2):53–83.[CrossRef]
[14] Martins M. Behavioral institutions and refinements in generalized hidden logics. J. Univers. Comput. Sci. (2006) 12(8):1020–1049.
[15] Leavens G., Pigozzi D. The behavior-realization adjunction and generalized homomorphic relations. Theor. Comput. Sci. (1997) 177:183–216.[CrossRef]
[16] Leavens G., Pigozzi D. A complete algebraic characterization of behavioral subtyping. Acta Inf. (2000) 36:617–663.[CrossRef]
[17] Casanovas E., Dellunde P., Jansana R. On elementary equivalence for equality-free logic. Notre Dame J. Form. Log. (1996) 37:506–522.[CrossRef]
[18] Malcolm G. Behavioural Equivalence, Bisimulation, and Minimal Realisation. Magne Haveraaen, Olaf Owe, Ole-Johan Dahl, eds. (1996) Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types 1995, September. 359–378.
[19] Schoett O. Behavioural correctness of data representations. Sci. Comput. Program. (1990) 14:43–57.[CrossRef]
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||||||