We present an outline of a process by which operational software requirements specifications can be written for Formal Concept Analysis (FCA). The Z notation is used to specify the FCA model and the formal operations on it. We posit a novel approach whereby key features of Z and FCA can be integrated and put to work in contemporary software development, thus promoting operational specification as a useful application of conceptual structures.
The Z notation is a method of formally specifying software systems [
An issue with formal methods has been the amount of effort required to produce a mathematical specification of the software system being developed. Having a ’ready made’ mathematical model provided by FCA would allow formal methods to have a new outlet. Whilst FCA can already be used to aid in the understanding and implementation of software systems (see next Section), Z can provide the method and structure by which FCA can be properly integrated into a development life cycle.
Work linking FCA and Z has been undertaken [
FCA has been used in a number of ways for software development; for modeling
the data structure of software applications, such as ICE [
Tilley et al [
One piece of work that does relate FCA directly to phases of the software life cycle has been carried out by Hesse and Tilley [12]; They discuss how FCA applies to requirements engineering and analysis. By taking a use-case approach, relating information objects to functional processes, they show that a hierarchical program structure can be produced. They suggest that FCA can play a central role in the software engineering process as a form of concept-based software development. The approach of this paper embodies their idea, with FCA providing the information structure and Z providing the process specification (Figure 1). In FCA a formal context consists of a set of objects, G , a set of attributes, M , and a relation between G and M , I ⊆ G × M . A formal concept is a pair (A, B ) where A ⊆ G and B ⊆ M . Every object in A has every attribute in B . For every object in G that is not in A, there is an attribute in B that that object does not have. For every attribute in M that is not in B there is an object in A that does not have that attribute. A is called the extent of the concept and B is called the intent of the concept. If g ∈ A and m ∈ B then (g , m) ∈ I , or gIm.
In Z, information structures are declared based upon a typed set theory. To apply this in FCA, G becomes such a type, namely the universal set of objects of interest. Similarly, M becomes the universal set of attributes that the objects of interest may have. The notation g : G declares an object g of type G and m : M declares an attribute m of type M . Sets can be declared using the powerset notation, P, and relations declared by placing an appropriate arrow between related types. 3.1
Using the Z notation, the formal context and concepts can be specified as state variables in a state schema (Figure 2), declaring the relation I , along with a concept function, S , which maps extents to intents. S is declared as an injection; an intent has one and only one extent, an extent has one and only one intent.The lower section of the schema (the schema predicate) logically describes how I and S are related. A : P G declares that A is a set of objects. B is the intent of A. | ContextAndConcepts I : G ↔ M S : P G 7 P M ∀ A : P G; B : P M | (A, B ) ∈ S • ∀ g : G; m : M • g ∈ A ∧ m ∈ B ⇔ gIm ∧ ∀ g : G | g ∈/ A • ∃ m : M | m ∈ B ∧ ¬ gIm ∧ ∀ m : M | m ∈/ B • ∃ g : G | g ∈ A ∧ ¬ gIm can be read as ’such that’ and • can be read as ’then’.
Although a proof is not attempted here, the predicate appears, by inspection, to satisfy Wille’s conditions for deriving concepts so that A = B I and B = AI [13]. 3.2
In Z, a query postfix, ?, is used to indicate an input to an operation and an exclamation postfix, !, is used to indicate an output from an operation. The symbol Ξ indicates that the operation does not change the value of the state variables.
In Z, if R is a binary relation between X and Y , then the domain of R (dom R) is the set of all members of X which are related to at least one member of Y by R. The range of R (ran R) is the set of all members of Y to which at least one member of X is related by R.
By making use of the concept function, S , and the fact that it is injective, operations to output the intent of an extent and to output the extent of an intent, are easily specified. Figure 3 specifies the latter in an operation schema called FindExtent.
A strength of the Z notation is its notion of preconditions and postconditions. Preconditions are statements that must be true for the operation to be successful and postconditions specify the result of the operation. In FindExtent, the precondition B ? ∈ ran S states that the input set of attributes must be in the range of S . The postcondition A! = S ∼(B ?) obtains the extent by inverting S and supplying it with the intent.
FindIntent is not specified here as it is, essentially, a mirror of FindExtent, with the input being a set of objects and the output being the corresponding set of attributes, B ! = S (A?).
FindExtent ΞContextAndConcepts B ? : P M A! : P G B ? ∈ ran S A! = S ∼(B ?) FindAttributes ΞContextAndConcepts g? : G B ! : P M g? ∈ dom I B ! = I (| {g?} |)
A query operation that outputs an object’s attributes, called FindAttributes is shown in Figure 4. The set of attributes is obtained by taking the relational image of I through a set containing the object of interest. Again, the operation FindObjects (for an attribute of interest) is similar and is not specified here.
Operation schemas to find object concepts and attribute concepts can be specified according to Wille’s definitions, γg := ({g }II , {g }I ) and γm := ({m}II , {m}I ), by piping together the corresponding object/attribute, extent/intent queries using a chevron notation, >>. The output from the schema preceding the chevrons becomes the input for the schema that follows them:
FindObjectConcept =b FindAttributes >> FindExtent ,
FindAttributeConcept =b FindObjects >> FindIntent .
In each case, we are interested in the outputs of both of the piped schemas, so that γg = (A!, B !?) and γm = (A!?, B !). The postfix !? indicates that something is first an output and then an input. 3.3
A strength of the Z notation is its notion of before and after states, i.e. a clear distinction is made between the value of state variables before an operation is carried out and their values after the operation is carried out. A state variable decorated with an apostrophe indicates that is in the after state. The symbol Δ indicates that an operation changes the state.
An operation to add a new object to the context can be specified by declaring the object and the object’s attributes as inputs. The operation schema AddObject is shown in Figure 5. It is a precondition that the attributes currently exist in the context.
In Z, −⊲ subtracts elements from a range and ⊲ restricts a range. These are used in the postcondition involving S to take into account the possibility that the attributes of the new object are an existing intent. The relevant concept is updated by adding the new object to the corresponding extent.
AddObject ΔContextAndConcepts g? : G B ? : P M g? ∈/ dom I B ! ⊆ ran I I ′ = I ∪ { m : M | m ∈ B ! • g? 7→ m } S ′ = (S ⊲− {B ?}) ∪ {S(dom S ⊲ {B ?}) ∪ {g?} 7→ B ?}
A similar operation to add a new attribute can be specified, but is not given here. Other useful operations that can be specified include those to remove an object from the context, remove an attribute from the context, remove an attribute from an object, remove an object from an attribute and to add an existing attribute to an existing object. It also is possible that other notions in FCA, such as the superconcept/subconcept relationship and attribute/object implications, will lend themselves to operational specification in Z. 4
Consider a user profile system where users belong to groups and groups are associated with services. The contexts for this system are usergroupContext : USER ↔ GROUP groupserviceContext : GROUP ↔ SERVICE
The complete state schema UserProfileSystem is not given for the sake of brevity. The concept functions are also omitted (in practice, where concepts are explicitly required, it may be more pragmatic to specify an axiom to obtain them from the context, rather than include them explicitly in the system state).
An operation is required to form a new group from all users who have access to a particular set of services. The preconditions are that the group must not already exist and that there must be at least one user who has access to the set of services (this also ensures that the services exist). The requirement is specified in Figure 6.
FormGroup ΔUserProfileSystem newgroup? : GROUP services? : P SERVICE newgroup? ∈/ dom groupserviceContext usergroupcontext 9o groupservicecontext ⊲ services? = ∅ ∃ user : USER | services? ⊆
ran({user } ⊳ usergroupContext 9o groupserviceContext) usergroupContext′ = usergroupContext ∪ {user : USER | services? ⊆
ran({user } ⊳ usergroupContext 9o groupserviceContext) • user 7→ newgroup?} groupserviceContext′ = groupserviceContext ∪ {service : SERVICE | service ∈ services? • newgroup? 7→ service}
Relational composition is carried out using 9o, here to form the relation between users and services. ⊳ is domain restriction. Set comprehension is used in the postconditions in the form {... • x 7→ y }. The mapping x 7→ y defines the form of the elements of the comprehended set.
The above example shows how formal contexts, arising from FCA, can be used in the formal specification of system requirements. The operation schema FormGroup is an unambiguous specification that can be translated into a program design.
The work presented here paves a way by which an FCA model can be specified as a Z state schema and that operations on the model (system requirements) can then be specified as Z operation schemas. The strengths of the conceptual model are thus combined with the strengths of structured formal methods. The Z notation is well understood as part of the software life cycle; it has strengths in the way functional system requirements are structured as schemas and in its notions of pre and post conditions and before and after states. Z has an industry standard and is supported by a variety of software engineering tools. We therefore envisage FCA systems that are specified using Z as opening up FCA to the comprehensive tools and support that are available for Z and vice versa, thereby promoting operational requirements specification as a useful application of conceptual structures. 12. W. Hesse and T. Tilley. Formal Concept Analysis Used for Software Analysis and Modelling. In B. Ganter, G. Stumme and R. Wille, editors, Formal Concept Analysis: Foundations and Applications, pages 288-303. Springer-Verlag, Germany, 2005. 13. R. Wille. Formal Concept Analysis as Mathematical Theory of Concepts and Concept Hierarchies. In B. Ganter, G. Stumme and R. Wille, editors, Formal Concept Analysis: Foundations and Applications, pages 1-33. Springer-Verlag, Germany, 2005.