Unit Testing for Casl Architectural Specifications

Patricia D.L. Machado^{1} and Donald Sannella^{2}

1 Systems and Computing Department, Federal University of Paraiba 2 Laboratory for Foundations of Computer Science, University of Edinburgh

Abstract. The problem of testing modular systems against algebraic specifications is discussed. We focus on systems where the decomposition into parts is specified by a Casl-style architectural specification and the parts (units) are developed separately, perhaps by an independent supplier. We consider how to test such units without reference to their context of use. This problem is most acute for generic units where the particular instantiation cannot be predicted.

1 Introduction

Formal testing is concerned with deriving test cases from formal specifications and checking whether programs satisfy these test cases for a selected finite set of data, as a practical alternative to formal proof. Much work has focused on test case selection and (automatic) interpretation of test results. Testing from algebraic specifications has been investigated, focusing on both “flat” specifications [Ber89,Gau95,LA96,Mac99] and structured specifications [LA96,Mac00b,DW00]. It is often assumed that the structure of the specification matches the structure of the program [LeG99,DW00] although it is possible to take specification structure into account without making this strong assumption [Mac00b].

Tests are not interesting unless we can interpret their results in terms of correctness. Oracles are decision procedures for interpreting the results of tests. The oracle problem arises whenever a finite executable oracle cannot be defined; this may stem e.g. from the semantic gap between specification and program values. Guaranteeing correctness by testing requires tests covering all possible interactions with the system, usually an infinite and impractical activity. When only finite sets of interactions are considered, successful testing can accept incorrect programs and unsuccessful testing can reject correct programs. The latter must be avoided since the costs of finding and fixing errors are too high to waste effort on non-errors. Accepting incorrect programs is not a problem as long as test coverage is adequate, since testing is not expected to guarantee correctness.

This paper addresses testing of modular systems where parts are developed independently from Casl-style architectural specifications [ABK^{+}03,BST02]. In this context, the problem reduces to that of testing units independently in such a way that their integration can be checked in a cost-effective way. An architectural specification consists of a list of unit declarations, naming the units (components) that are required with specifications for each of them, together with a unit term that describes the way in which these units are to be combined.

When testing modular systems and their parts, different perspectives need to be considered. From a supplier’s point of view, units have to be checked independently of their contexts of use. Checking generic units poses special problems since the particular instantiation is unknown in general, and the set of all possible instantiations is almost always infinite. In this paper, we present styles of testing non-generic and generic units that address these problems. The main novelty is in the case of generic units. Integration testing is left to future work. A extended version of this paper with examples demonstrating most of the main definitions and results is available as an Edinburgh technical report.

2 Preliminary definitions

Algebraic Specifications. We assume familiarity with basic concepts and notation of algebraic specification, where programs are modelled as algebras. Each signature Σ = (S, F, Obs) is equipped with a distinguished set Obs ⊆ S of observable sorts. Sign is the category of signatures. We consider specifications with axioms of first-order equational logic, and write Sen(Σ) for the set of all Σ-sentences. We restrict to algebras with non-empty carriers, and write Alg(Σ) for the class of all such Σ-algebras. [A] denotes the reachable subalgebra of A ∈ Alg(Σ). Behavioural Equality. For a non-observable sort, it is not appropriate to assume that equality on values is the usual set-theoretical one. Equality on values of a Σ-algebra A can be interpreted by an appropriate behavioural equality, a partial Σ-congruence ≈_{A} = (≈_{A,s})_{s∈S} with Dom(≈_{A}) = {a | a ≈_{A} a}. The partial observational equality ≈_{Obs,A}= (≈_{Obs,A,s})_{s∈S} is one example of a behavioural equality, where related elements are those that cannot be distinguished by observable computations.^{3} A Σ-behavioural equality is defined as ≈_{Σ} = (≈_{Σ,A})_{A∈Alg(Σ)}, one behavioural equality for each Σ-algebra A. Approximate Equality. Behavioural equality can be difficult to test. Consider e.g. observational equality on non-observable sorts, defined in terms of a set of contexts that is usually infinite. One approach involves the use of approximate equalities [Mac99,Mac00c] which are binary relations on values of the algebra. An approximate equality is sound with respect to a behavioural equality if all values (in Dom(≈_{A})) that it identifies are indeed equal, or complete if all equal values are identified. Any contextual equality ∼_{C,A} defined from a subset C of the observable computations^{4} is complete with respect to observational equality, although it need not be a partial congruence. The set-theoretical equality is sound – in programming terms, this is equality on the underlying data representation.

3 Let C_{Obs} be the set of all Σ-contexts T_{Σ}(X ∪ {z_{s}}) of observable sorts with context variable z_{s} of sort s. Then values a and b of sort s are observationally equal, a ≈_{Obs,A,s} b, iff a, b ∈ [A] and ∀C ∈ C_{Obs}· ∀α : X → [A] · α_{a}^{#}(C) = α_{b}^{#}(C), where α_{a}, α_{b} : X ∪ {z_{s}} → [A] are the extensions of α defined by α_{a}(z_{s}) = a and α_{b}(z_{s}) = b.

4 Let C ⊆ C_{Obs}. Values a and b are contextually equal w.r.t C iff a, b ∈ [A] and ∀C ∈ C·∀α : X → [A]·α_{a}^{#}(C) = α_{b}^{#}(C). Obviously, if C = C_{Obs}, then ∼_{C,A} = ≈_{Obs,A}.

Families of Equalities. The signature of different parts of a structured specification may differ, and the interpretation of equality (e.g. observational equality) may depend on the signature. So, to deal with structured specifications, we use families of equalities indexed by signatures. Let ≈ = (≈_{Σ})_{Σ∈Sign} be a family of behavioural equalities and let ∼ = (∼_{Σ})_{Σ∈Sign} and ≏ = (≏_{Σ})_{Σ∈Sign} denote arbitrary families of approximate equalities. The family ∼ is complete (sound) w.r.t. ≈ if ∼_{Σ} is complete (sound) w.r.t. ≈_{Σ} for all Σ. The reduct of ∼_{Σ} by σ : Σ′ → Σ is (∼_{Σ})|_{σ} = ((∼_{Σ,A})|_{σ})_{A∈Alg(Σ)} where (∼_{Σ,A})|_{σ} = ((∼_{Σ,A})_{σ(s)})_{s∈S′}; then the family ∼ is compatible with signature morphisms if for all σ : Σ′ → Σ and all A ∈ Alg(Σ), ∼_{Σ′,A|_{σ}} = (∼_{Σ,A})|_{σ}. For the results below having compatibility as a condition, it is enough to consider the signatures arising in the structure of a given specification (for a normalized specification, this includes intermediate signatures arising during normalization). Compatibility may fail if these signatures have different sets of observers for the same sort. The family of set-theoretical equalities is always compatible, but it is easy to check that the family of observational equalities is not compatible in general. One may restrict the introduction of new observers to avoid this problem, see e.g. [BH99].

3 Formal Testing from Algebraic Specifications

Testing from algebraic specifications boils down to checking if axioms are satisfied by programs [Gau95]. Oracles are usually active procedures which drive the necessary tests and interpret the results. Test cases are extracted from specifications together with test sets defined at specification level and associated with axioms. Then, oracles are defined for each test case or group of test cases. A test obligation combines a test case, test data, a test oracle and a program to be tested. When there is no chance of confusion, this is referred to simply as a test. Test Cases and Test Data. For simplicity, each axiom is regarded as a separate test case. Techniques exist to simplify test cases or make them more practical, but this is a separate topic. Test data sets are usually defined from specifications rather than from programs. Here, test sets will be taken to be sets of ground terms [Gau95,Mac99] corresponding to sets of values in the program under test. Test Oracle Design. The oracle problem often reduces to the problem of comparing values of a non-observable sort for equality; when equality is interpreted as behavioural equality, e.g. observational equality, it may be difficult or impossible to decide. Quantifiers ranging over infinite domains make the oracle problem more difficult. An approach to defining oracles that addresses these problems is presented in [Mac99], where equality is computed using two approximate equalities, one sound and one complete. These equalities are applied according to the context in which equations occur, positive or negative^{5}. To handle the quantifier

5 A context is positive if it is formed by an even number of applications of negation (e.g. ϕ is in a positive context in both ϕ ∧ ψ and ¬¬ϕ). Otherwise, the context is negative. Note that ϕ is in a negative context and ψ is in a positive context in ϕ ⇒ ψ since it is equivalent to ¬ϕ ∨ ψ. A formula or symbol occurs positively (resp. negatively) in ϕ if it occurs in a positive (resp. negative) context within ϕ.

problem, restrictions are placed on the contexts in which they can occur. An approximate oracle is then a procedure that decides whether a given axiom is satisfied by a program or not. Such an oracle computes a “testing satisfaction” relation (given below) which differs from the standard one in the way equality is computed and also because quantifiers range only over given test sets.

Definition 3.1 (Testing Satisfaction). Let Σ be a signature, T ⊆ T_{Σ} be a Σ-test set, ∼, ≏ be two Σ-approximate equalities, A be a Σ-algebra and α : X → Dom(≈_{A}) be a valuation. Testing satisfaction ⊧_{∼,≏}^{T} is defined as follows.

1. A, α ⊧_{∼,≏}^{T} t = t′ iff α^{#}(t) ∼_{A} α^{#}(t′);

2. A, α ⊧_{∼,≏}^{T} ¬ψ iff A, α ⊧_{≏,∼}^{T} ψ does not hold;

3. A, α ⊧_{∼,≏}^{T} ψ_{1} ∧ ψ_{2} iff both A, α ⊧_{∼,≏}^{T} ψ_{1} and A, α ⊧_{∼,≏}^{T} ψ_{2} hold;

4. A, α ⊧_{∼,≏}^{T} ∀x:s · ψ iff A, α[x ↦ ^{#}(t)] ⊧_{∼,≏}^{T} ψ holds for all t ∈ T_{s}

where α[x ↦ v] is the valuation α superseded at x by v. Satisfaction of formulae involving ∨, ⇒, ⇔, ∃ is given using their definitions in terms of ¬, ∧, ∀. Note that ∼ is always applied in positive contexts and ≏ is always applied in negative contexts: the approximate equalities are reversed when negation is encountered.

The following theorem relates testing satisfaction to usual behavioural satisfaction (⊧_{≈}), where equality is interpreted as behavioural equality (≈) and quantification is over all of Dom(≈).

Theorem 3.2 ([Mac99]). If ∼ is complete, ≏ is sound, and ψ has only positive occurrences of ∀ and negative occurrences of ∃, then A, α ⊧_{≈} ψ implies A, α ⊧_{∼,≏}^{T} ψ. ⊓ ⊔

The restriction to positive ∀ and negative ∃ here and in later results is not a problem in practice, since it is satisfied by most common specification idioms.

4 Testing from Non-Generic Unit Specifications

This section discusses testing non-generic program units against specifications without considering the internal modular structure of the units. The styles of testing presented can be used to test the individual units of a modular system.

Good practice requires units to be checked independently of their contexts of use. For formal (functional) testing, this corresponds to checking whether the unit satisfies its specification. Testing from flat specifications can follow directly the approach presented in Sect. 3 for each test case. However, once structured specifications are considered, there are additional complications. First, the structure has to be taken into account when interpreting test results w.r.t. specification axioms. Also, in order to check axioms that involve “hidden symbols” it is necessary to provide an additional implementation for these symbols as the program under test is not required to implement them.

Structured specifications are built using structuring primitives like renaming, union, exporting and extension. These provide a powerful mechanism for reusing and adapting specification as requirements evolve. In structured specifications with testing interface [Mac00b], test sets are incorporated into specifications.

Definition 4.1 (Structured Specifications with Testing Interface). The syntax and semantics of structured specifications are inductively defined as follows. Each specification SP is assigned a signature Sig(SP) and two classes of Sig(SP)-algebras. Mod_{≈}(SP) is the class of “real” models of SP w.r.t. the family of Σ-behavioural equalities ≈ = (≈_{Σ})_{Σ∈Sign}, and ChMod_{∼,≏}(SP) is the class of “checkable” models of SP determined by testing w.r.t. the families of approximate equalities ∼ = (∼_{Σ})_{Σ∈Sign} and ≏ = (≏_{Σ})_{Σ∈Sign} and the test sets associated with each axiom.

1. (Basic) SP = ⟨Σ, Ψ⟩ with Ψ ⊆ {(ψ, T) | ψ ∈ Sen(Σ) and T ⊆ T_{Σ}}. – Sig(SP) = Σ

– Mod_{≈}(SP) = {A ∈ Alg(Σ) | ⋀_{(ψ,T)∈Ψ} A ⊧_{≈} ψ}

– ChMod_{∼,≏}(SP) = {A ∈ Alg(Σ) | ⋀_{(ψ,T)∈Ψ} A ⊧_{∼,≏}^{T} ψ}

2. (Union) SP = SP_{1} ∪SP_{2}, where SP_{1} and SP_{2} are structured specifications, with Sig(SP_{1}) = Sig(SP_{2}).

– Sig(SP) = Sig(SP_{1}) [= Sig(SP_{2})]

– Mod_{≈}(SP) = Mod_{≈}(SP_{1}) ∩ Mod_{≈}(SP_{2})

– ChMod_{∼,≏}(SP) = ChMod_{∼,≏}(SP_{1}) ∩ ChMod_{∼,≏}(SP_{2})

3. (Renaming) SP = translate SP′ with σ, where σ : Sig(SP′) → Σ. – Sig(SP) = Σ

– Mod_{≈}(SP) = {A ∈ Alg(Σ) | A|_{σ} ∈ Mod_{≈}(SP′)}

– ChMod_{∼,≏}(SP) = {A ∈ Alg(Σ) | A|_{σ} ∈ ChMod_{∼,≏}(SP′)}

4. (Exporting) SP = SP′|_{Σ}, where Σ is a subsignature of Sig(SP′). – Sig(SP) = Σ

– Mod_{≈}(SP) = {A′|_{Σ} | A′ ∈ Mod_{≈}(SP′)}

– ChMod_{∼,≏}(SP) = {A′|_{Σ} | A′ ∈ ChMod_{∼,≏}(SP′)}

Operations presented in Definition 4.1 are primitive ones and, in practice, more complex operations, defined from their combination, are found in Casl and other languages. Extension – “then” in Casl – is defined in terms of renaming and union: SP′ then sorts S opns F axioms Ψ =^{def} ⟨Σ, Ψ⟩ ∪ translate SP′ with σ, where SP′ is a structured specification, S is a set of sorts, F is a set of function declarations, Σ = Sig(SP′) ∪ (S, F), σ : Sig(SP′) ↪ Σ is the inclusion, and Ψ is a set of axioms over Σ with their associated test sets. The union of specifications over possibly different signatures – “and” in Casl – can be expressed as: SP_{1} and SP_{2} =^{def} translate SP_{1} with σ_{1} ∪ translate SP_{2} with σ_{2}, where Σ = Sig(SP_{1}) ∪ Sig(SP_{2}) and σ_{1} : Sig(SP_{1}) ↪ Σ, σ_{2} : Sig(SP_{2}) ↪ Σ.

To handle the oracle problem for structured specifications, two styles of testing are suggested in [Mac00b]: structured and flat testing. Structured testing of a Σ-algebra A against a structured specification SP corresponds to membership in the class of checkable models of SP, i.e., A ∈ ChMod_{∼,≏}(SP). Structured testing is based on the structure of SP; it may involve more than one set of test obligations (see Definition 4.1) and may demand additional implementation of symbols not in A (not exported by SP).

On the other hand, flat testing takes a monolithic approach based on an unstructured view of the specification without considering non-exported symbols and using a single pair of approximate equalities on the overall signature of SP. More specifically, flat testing corresponds to testing satisfaction of axioms extracted from SP, i.e., ⋀_{(ψ,T)∈TAx(SP)} A ⊧_{∼_{Σ},≏_{Σ}}^{T} ψ where Σ = Sig(SP) and TAx(SP) are the visible axioms of SP, defined as follows.

Definition 4.2 (Visible Axioms). The set of visible axioms together with corresponding test sets of a specification SP is defined as follows.

1. TAx(⟨Σ, Ψ⟩) = Ψ

2. TAx(SP_{1} ∪ SP_{2}) = TAx(SP_{1}) ∪ TAx(SP_{2})

3. TAx(translate SP′ with σ) = σ(TAx(SP′))

4. TAx(SP′|_{Σ}) = {(ϕ, T ∩ T_{Σ}) | (ϕ, T) ∈ TAx(SP′) and ϕ ∈ Sen(Σ)}

The visible axioms of a specification SP exclude those that refer to non-exported symbols, translating the rest to the signature of SP.

Whether structured or flat testing is performed, we must ask: under which conditions are correct models not rejected by testing? Results in [Mac00b,Mac00c] show that under certain assumptions, structured testing and flat testing do not reject correct models, even though incorrect ones can be accepted.

Theorem 4.3 ([Mac00b]). If ∼ is complete, ≏ is sound, and the axioms of SP have only positive occurrences of ∀ and negative occurrences of ∃, then A ∈ Mod_{≈}(SP) implies A ∈ ChMod_{∼,≏}(SP). ⊓ ⊔

Theorem 4.4 ([Mac00b]). If ∼ is complete and compatible and ≏ is sound and compatible and the axioms of SP have only positive occurrences of ∀ and negative occurrences of ∃, then A ∈ Mod_{≈}(SP) implies ⋀_{(ψ,T)∈TAx(SP)} A ⊧_{∼,≏}^{T} ψ. ⊓ ⊔

Structured testing is more flexible than flat testing in the sense that fewer assumptions are made. The family of observational equalities is not compatible as mentioned in Sect. 2, so the additional assumption is a strong one. On the other hand, flat testing is simpler. Both theorems cover a prevalent use of quantifiers. Their duals also hold, but are less interesting. There are also variants of these theorems that substitute assumptions on test sets for assumptions on quantifiers.

Structured testing and flat testing are two extremes. In practice, we may combine them. This can be done via normalization, where a structured specification SP is transformed into a specification nf (SP) of the form ⟨Σ′, Ψ′⟩|_{Σ} [BCH99] having the same signature and class of models. This procedure groups axioms, taking hidden symbols into account, so that the result is a flat specification which exports visible symbols. The usual normalization procedure is easily extended to structured specifications with testing interface (see [Mac00a] for details) and then we obtain the following result:

Theorem 4.5 ([Mac00a]). If ∼ and ≏ are compatible, then ChMod_{∼,≏}(SP) = ChMod_{∼,≏}(nf(SP)). ⊓ ⊔

The main advantage of normal form is to allow a combination of compositional and non-compositional testing, namely semi-structured testing, where normal forms are used to replace parts of a specification, especially when these parts are combined by union. The result is to reduce the number of different experiments that are performed. Then, the resulting specification can be checked by structured testing and a result analogous to Theorems 4.3 and 4.4 is obtained:

Theorem 4.6 ([Mac00a]). If ∼ is complete, ≏ is sound, ≈ is compatible and the axioms of SP have only positive occurrences of ∀ and negative occurrences of ∃, then A ∈ Mod_{≈}(SP) implies A ∈ ChMod_{∼,≏}(nf(SP)). ⊓ ⊔

Even though we have shown theoretical results regarding structured, flat and semi-structured testing, these styles of testing can be infeasible in practice when the structure of the program is not taken into account, since it may be necessary to decompose the program to reflect certain signatures in the structure of the specification and/or re-test the whole program every time it is modified.

5 Testing from Generic Unit Specifications

This section is concerned with testing generic units independent of particular instantiations. This is a difficult task for testing since we have to anticipate the behaviour of a generic unit when instantiated by specific units, but the set of all possible instantiations is almost always infinite. Not all units having the right signature are correct implementations of the argument specification, and correctness cannot generally be determined by testing. However, testing a generic unit using an incorrect implementation of the argument specification may lead to rejection of correct generic units.

The syntax and semantics of generic unit specifications are as follows. First, let Alg(Σ′ → Σ) = {F : Alg(Σ′) ⇀ Alg(Σ) | ∀A ∈ Dom(F), F [A]|_{Σ′} = A} be the class of persistent partial functions taking Σ′-algebras to Σ-algebras, where Σ′ ⊆ Σ. These functions on algebras model generic units; they are partial since a generic unit is only required to produce a result when instantiated by an algebra that satisfies the argument specification.

Definition 5.1 (Generic Unit Specifications). Let Sig(SP) = Σ and Sig(SP′) = Σ′, such that SP extends SP′, i.e. Σ′ ⊆ Σ and for all A ∈ Mod_{≈}(SP), A|_{Σ′} ∈ Mod_{≈}(SP′).

– Sig(SP′ → SP) = Σ′ → Σ

– Mod_{≈}(SP′ → SP) = {F ∈ Alg(Σ′ → Σ) | ∀A ∈ Mod_{≈}(SP′), A ∈ Dom(F) and F [A] ∈ Mod_{≈}(SP)}

– ChMod_{∼,≏}(SP′ → SP) = {F ∈ Alg(Σ′ → Σ) | ∀A ∈ ChMod_{∼,≏}(SP′), A ∈ Dom(F) and F [A] ∈ ChMod_{∼,≏}(SP)}

Let SP′ → SP be a generic unit specification and let F be a generic unit that is claimed to correctly implement this specification. In contrast to testing from non-generic unit specifications, membership in the class of checkable models does not give rise to a feasible style of testing from generic unit specifications. First, the class of models of SP′ may be infinite. Moreover, the class of checkable models of SP′ → SP cannot be directly compared to its class of “real” models. Suppose F ∈ Mod_{≈}(SP′ → SP) and A ∈ ChMod_{∼,≏}(SP′), but A ∉ Mod_{≈}(SP′) and F [A] ∉ ChMod_{∼,≏}(SP). Then, F ∉ ChMod_{∼,≏}(SP′ → SP) – a correct F is rejected due to bugs in A.

As explained earlier, a testing method should ensure that correct models are not rejected. This requires that incorrect models of the parameter specification are not used in testing. Suppose another class of models, named strong models, is defined as an alternative to the class of checkable models.

Definition 5.2 (Strong Models). The class of strong models of SP′ → SP is defined as SMod_{∼,≏}(SP′ → SP) = {F ∈ Alg(Σ′ → Σ) | ∀A ∈ Mod_{≈}(SP′), A ∈ Dom(F) and F [A] ∈ ChMod_{∼,≏}(SP)}.

This represents the class of models which are successfully tested when only correct implementations of SP′ are considered. We then have:

Theorem 5.3. If ∼ is complete, ≏ is sound, and the axioms of SP have only positive occurrences of ∀ and negative occurrences of ∃, then F ∈ Mod_{≈}(SP′ → SP) implies F ∈ SMod_{∼,≏}(SP′ → SP).

Proof. Suppose F ∈ Mod_{≈}(SP′ → SP). Then, ∀A ∈ Mod_{≈}(SP′), A ∈ Dom(F) and F [A] ∈ Mod_{≈}(SP). By Theorem 4.3, F [A] ∈ ChMod_{∼,≏}(SP). Hence, F ∈ SMod_{∼,≏}(SP′ → SP). ⊓ ⊔

This means that if we can test for membership in the class of strong models, then correct models of generic unit specifications are not rejected. Obviously, incorrect models can be accepted. As with Theorem 4.3, the dual also holds.

In practice, testing membership in SMod_{∼,≏}(SP′ → SP) (this also applies to ChMod_{∼,≏}(SP′ → SP)) is not possible, since as already noted the class Mod_{≈}(SP′) is almost always infinite and in any case membership in this class is not testable in general. A feasible approach to test whether generic units are models of SP′ → SP should only rely on a finite subset of Mod_{≈}(SP′). So let C be a set of units (“stubs”) chosen according to some coverage criteria. Then we define a “weak” class of models of SP′ → SP as follows.

Definition 5.4 (Weak Models). Let C ⊆ Mod_{≈}(SP′). The class of weak models of SP′ → SP is defined as W Mod_{∼,≏,C}(SP′ → SP) = {F ∈ Alg(Σ′ → Σ) | ∀A ∈ C, A ∈ Dom(F) and F [A] ∈ ChMod_{∼,≏}(SP)}.

The intention here is to select a class C which is finite and has a reasonable size such that F can be tested with this class and useful information gained. The following theorem shows that under certain assumptions, correct generic units are not rejected by testing w.r.t. the class of weak models.

Theorem 5.5. If ∼ is complete, ≏ is sound, and the axioms of SP have only positive occurrences of ∀ and negative occurrences of ∃, then F ∈ Mod_{≈}(SP′ → SP) implies F ∈ W Mod_{∼,≏,C}(SP′ → SP) for any C ⊆ Mod_{≈}(SP′).

Proof. Suppose F ∈ Mod_{≈}(SP′ → SP). Then, ∀A ∈ C ⊆ Mod_{≈}(SP′), A ∈ Dom(F) and F [A] ∈ Mod_{≈}(SP). By Theorem 4.3, F [A] ∈ ChMod_{∼,≏}(SP). Hence, F ∈ W Mod_{∼,≏,C}(SP′ → SP). ⊓ ⊔

The class of weak models is comparable to the classes of checkable and strong models, i.e., for any C ⊆ Mod_{≈}(SP′), F ∈ ChMod_{∼,≏}(SP′ → SP) implies F ∈ W Mod_{∼,≏,C}(SP′ → SP), provided the assumptions of Theorem 4.3 hold for SP′, and F ∈ SMod_{∼,≏}(SP′ → SP) implies F ∈ W Mod_{∼,≏,C}(SP′ → SP). Moreover, for any algebra A used to test membership of F in the class of weak models of SP′ → SP, we can conclude that F [A] is indeed a checkable model of SP, i.e., if A ∈ C and F ∈ W Mod_{∼,≏,C}(SP′ → SP) then F [A] ∈ ChMod_{∼,≏}(SP), by Definition 5.4. However, what if A ∈ Mod_{≈}(SP′), but A ∉ C? Is F [A] ∈ ChMod_{∼,≏}(SP)? How do we select an appropriate finite set of Sig(SP′)-algebras so that an answer to the above question can be given?

Even though, under the assumptions of Theorem 5.5, testing membership in the class of weak models does not reject correct programs, not all sets C of stubs are equally interesting. It is desirable that a generic unit F be tested without regard to the units that are going to be used to instantiate it subsequently. Then, if we can conclude that F [A] is a checkable model for some A, it may be possible to avoid re-testing F when A is replaced by a different unit. In other words, we need to select C to be a representative subset of Mod_{≈}(SP′) so that given a correct realisation A of SP′ (A ∈ Mod_{≈}(SP′)) and a generic unit F in the class of weak models of SP′ → SP (F ∈ W Mod_{∼,≏,C}(SP′ → SP)), we can conclude that F [A] is a realisation of SP (F [A] ∈ ChMod_{∼,≏}(SP)).

One possible answer to the above questions might be to pick one representative of every equivalence class w.r.t. an equivalence relation ≡ on algebras when defining C. This might be the observational equivalence on algebras [BHW95] or an approximation to it. The idea is similar to equivalence partitioning of test sets and the uniformity hypothesis in black-box testing [Ber91].

Let ≡ be an equivalence relation and define the closure of C under ≡ as Cl_{≡}(C) = {A ∈ Alg(Σ) | ∃B ∈ C ·A ≡ B}. In particular, we might pick C so that Cl_{≡}(C) coincides with Mod_{≈}(SP). Following [BHW95], we focus on equivalence relations that are “factorizable” by partial congruences of interest. The idea comes from automata theory: two finite state machines are equivalent (i.e. accept the same language) iff quotienting each one by the Nerode equivalence on states yields isomorphic machines. (In fact, we will require only right factorizability.)

Definition 5.6 (Factorizability). An equivalence ≡ ⊆ Alg(Σ) × Alg(Σ) is factorizable by a family of partial Σ-congruences ≈ = (≈_{A})_{A∈Alg(Σ)} if A ≡ B iff A/≈_{A} ≅ B/≈_{B}; ≡ is right factorizable by ≈ if A ≡ B implies A/≈_{A} ≅ B/≈_{B}.

It is shown in [BHW95] that various definitions of observational equivalence are factorizable by corresponding observational equalities. We will need an equivalence that is right factorizable by an approximate equality that is complete with respect to our chosen behavioural equality. Complete equalities are coarser than ≈, and if ≈ is observational equality then equivalences that are factorizable by such equalities are coarser than observational equivalence. Requiring right factorizability permits the equivalence to be finer than the factorizable one, including observational equivalence and equivalences finer than that.

The following theorem relates behavioural satisfaction of a sentence and ordinary satisfaction of the same sentence in a quotient algebra.

Theorem 5.7 ([BHW95]). Let ≈ = (≈_{A})_{A∈Alg(Σ)} be a family of partial Σcongruences. Then A/≈_{A} ⊧ ψ iff A ⊧_{≈} ψ. ⊓ ⊔

Putting these together:

Corollary 5.8. Let ≡ be right factorizable by ≈. Then A ≡ B implies A ⊧_{≈} ψ iff B ⊧_{≈} ψ.

Proof. A ⊧_{≈} ψ iff A/≈_{A} ⊧ ψ (Theorem 5.7) iff B/≈_{B} ⊧ ψ (A ≡ B, right factorizability, preservation of satisfaction by ≅) iff B ⊧_{≈} ψ (Theorem 5.7). ⊓ ⊔

Theorem 5.9. Let ≡ be right factorizable by ∼. Then A ≡ B implies A ∈ ChMod_{∼,∼}(SP) iff B ∈ ChMod_{∼,∼}(SP).

Proof. By induction on the structure of SP, using Corollary 5.8 for specifications of the form ⟨Σ, Ψ⟩. Since test sets are finite sets of ground terms, A ⊧_{∼,∼}^{T} ψ is equivalent to A ⊧_{∼} ψ′ where ψ′ is obtained from ψ by replacing each subformula of the form ∀x : s · φ by ⋀_{t∈T_{s}} φ[t/x] and each subformula of the form ∃x : s · φ by ⋁_{t∈T_{s}} φ[t/x]. ⊓ ⊔

A further assumption will be that generic units preserve ≡, i.e. are “stable”:

Definition 5.10 (Stability). A generic unit F ∈ Alg(Σ′ → Σ) is stable with respect to equivalences ≡_{Σ′} ⊆ Alg(Σ′) × Alg(Σ′) and ≡_{Σ} ⊆ Alg(Σ) × Alg(Σ) if for any A ∈ Dom(F), A ≡_{Σ′} B implies B ∈ Dom(F) and F [A] ≡_{Σ} F [B].

Stability with respect to observational equivalence is a reasonable assumption for generic units expressed in a programming language, since stability is closely related to the security of the data encapsulation mechanisms in that language, see [Sch87] and [ST97]. For an equivalence that is only an approximation to observational equivalence, stability seems reasonable as a hypothesis in the context of testing. We then have the main result of this section:

Theorem 5.11. Let C ⊆ Mod_{≈}(SP′). If F ∈ W Mod_{∼,∼,C}(SP′ → SP), A ∈ Cl_{≡_{Σ′}} (C), ≡ is right factorizable by ∼ and F is stable with respect to ≡_{Σ′} and ≡_{Σ}, then F [A] ∈ ChMod_{∼,∼}(SP).

Proof. A ∈ Cl_{≡_{Σ′}} (C) means that A ≡_{Σ′} B for some B ∈ C, and then F [B] ∈ ChMod_{∼,∼}(SP). By stability, F [A] ≡_{Σ} F [B]. Then, by Theorem 5.9, F [A] ∈ ChMod_{∼,∼}(SP). ⊓ ⊔

Corollary 5.12. Let C ⊆ Mod_{≈}(SP′). If F ∈ W Mod_{∼,∼,C}(SP′ → SP), ≡ is right factorizable by ∼ and F is stable with respect to ≡_{Σ′} and ≡_{Σ}, then F ∈ W Mod_{∼,∼,Cl_{≡}(C)}(SP′ → SP).

Theorem 5.11 and Corollary 5.12 are useful “amplification” results. They allow information gained from testing particular instantiations (the set of stubs C) to be extrapolated to give information about instantiations that have not actually been tested. Theorem 5.11 relates to the practice of replacing a module in a working system (in this case, the parameter of a generic unit) with another version. If the two versions can be shown to be equivalent (≡), then the overall system will continue to work provided the assumptions in Theorem 5.11 are met. In Corollary 5.12, if we choose C so that Cl_{≡}(C) = Mod_{≈}(SP), then the conclusion is equivalent to membership in the class of strong models of SP′ → SP. In most cases, this ideal will not be achievable; nevertheless, we can aim to include in C representatives of equivalence classes related to the particular class of applications for which F is intended to be used.

In order for testing to avoid rejecting correct units, according to Theorem 5.5 we need to restrict to specifications with only positive occurrences of ∀ and negative occurrences of ∃. A much more serious restriction when combining Theorems 5.5 and 5.11 is that ∼ needs to be both sound and complete. However, an analysis of the proof shows that it is sufficient if ∼ is complete for equations in positive positions and sound for equations in negative positions. If ≈ is observational equality then this can be achieved by taking ∼ to be a contextual equality (and hence complete) and restricting equations in negative positions to be of observable sorts only, for which ∼ is sound and complete.

6 Concluding remarks

We have presented ideas relating to testing modular systems against Casl-style architectural specifications. Our overall objective is to support independent development and verification of program components.

The problem of testing against architectural specifications reduces to:

1. testing non-generic units against structured specifications;

2. testing generic units against specifications of the form SP′ → SP; and

3. “integration testing” for unit terms that avoids re-testing.

Solutions to (1) are presented in Sect. 4, where previous results for testing against structured specifications are reviewed and discussed in the context of architectural specifications. Then, based on previous research on behavioural implementations, ideas concerning (2) are presented in Sect. 5. Since the class of possible parameter units (“stubs”) is almost always infinite, we suggest that a representative finite class be selected, allowing testing results to be extrapolated to equivalent units. For this, stability of generic units is assumed. Problem (3) is future work, although it is already clear that the results in Sect. 5 and [Mac00b,Mac00a,Mac00c] are relevant.

Other questions for the future concern the circumstances under which our approximation to stability holds, as well as the connection between equivalence on algebras and testing satisfaction, including the question of how this equivalence can be effectively checked. We also aim to extend the results to specifications of higher-order generic units. Finally, a general method of applying the ideas presented along with practical case studies are needed.

Acknowledgments: Thanks to Marie-Claude Gaudel for encouragement and to members of IFIP WG 1.3 for interesting questions. This research was partly funded by PROTEM-CC/CNPq.

References

[ABK^{+}03] E. Astesiano, M. Bidoit, H. Kirchner, B. Krieg-Brückner, P. Mosses, D. Sannella and A. Tarlecki. Casl: The common algebraic specification language. Theoretical Computer Science. To appear (2003).

[BB01] H. Baumeister and D. Bert. Algebraic specification in Casl. In Software Specification Methods – An Overview Using a Case Study. Springer (2001).

[Ber89] G. Bernot. A formalism for test with oracle based on algebraic specifications. Report 89-4, LIENS/DMI, Ecole Normale Supérieure, Paris (1989).

[Ber91] G. Bernot. Testing against formal specifications: a theoretical view. Proc. TAPSOFT’91, Brighton. Springer LNCS 494, 99–119 (1991).

[BCH99] M. Bidoit, M.V. Cengarle and R. Hennicker. Proof systems for structured specifications and their refinements. Algebraic Foundations of Systems Specifications, chapter 11. Springer (1999).

[BH99] M. Bidoit and R. Hennicker. Observational logic. Proc. AMAST’98, Manaus. Springer LNCS 1548, 263–277 (1999).

[BHW95] M. Bidoit, R. Hennicker and M. Wirsing. Behavioural and abstractor specifications. Science of Computer and Programming, 25:149–186 (1995).

[BST02] M. Bidoit, D. Sannella and A. Tarlecki. Architectural specifications in Casl. Formal Aspects of Computing. To appear (2002).

[DW00] M. Doche and V. Wiels. Extended institutions for testing. Proc. AMAST 2000. Springer LNCS 1816, 514–528 (2000).

[Gau95] M.-C. Gaudel. Testing can be formal, too. Proc. TAPSOFT’95, Aarhus. Springer LNCS 915 (1995).

[LeG99] P. LeGall. Vers une spécialisation des logiques pour spécifier formellement et pour tester des logiciels. Habilitation thesis, Université d’Evry (1999).

[LA96] P. LeGall and A. Arnould. Formal specification and test: correctness and oracle. Proc. WADT’95, Oslo. Springer LNCS 1130 (1996).

[Mac99] P.D.L. Machado. On oracles for interpreting test results against algebraic specifications. Proc. AMAST’98, Manaus. Springer LNCS 1548, 502–518 (1999).

[Mac00a] P.D.L. Machado. The rôle of normalisation in testing from structured algebraic specifications. Proc. WADT’99, Bonas. Springer LNCS 1827, 459–476 (2000).

[Mac00b] P.D.L. Machado. Testing from structured algebraic specifications. Proc. AMAST 2000. Springer LNCS 1816, 529–544 (2000).

[Mac00c] P.D.L. Machado. Testing from Structured Algebraic Specifications: The Oracle Problem. PhD thesis, LFCS, University of Edinburgh (2000).

[ST97] D. Sannella and A. Tarlecki. Essential concepts of algebraic specification and program development. Formal Aspects of Computing, 9:229–269 (1997).

[Sch87] O. Schoett. Data Abstraction and the Correctness of Modular Programming. PhD thesis, LFCS, University of Edinburgh (1987).