This paper describes the application of heterogeneous algebraic system for the construction of the formal model of object database instead of object algebra. Complete formalization of the operation of intersection of class specifications is given.
In applications of information technologies there is a problem of construction of the
so-called dependable and stable systems and infrastructures – the systems which
behave stably under all, especially, critical working circumstances. Similarity of risks
and increasing actuality of their decline to an acceptable level for critical applications
led to the appearance of a special term “safeware”, by the analogy with the terms
“hardware”, “software”, “firmware” etc., which combines two components: safe –
secure and ware – a product, an item. This term was suggested and patented by the
leading expert of NASA on the questions of infrastructure security, professor
N. Leveson, who registered the appearance of a modern field of knowledge called
safeware engineering [
For the full confidence in the fact that informational system will work stably (will
be dependable and stable), one should single out system components, describe them
formally and verify. Indeed, nowadays there is nothing instead of a “divide and rule”
approach to cope with this difficulty. In fact, one of the most important components
of any complex system (infrastructure) is databases. That’s why there should exist an
appropriate formal model. For the relational databases such a formal model has been
already constructed and explored considerably. This issue is exhaustively covered in
the literature, beginning from the pioneering works by E.F. Codd (see, e.g. [
Nowadays, there are a lot of formal models of object-oriented databases (OODB)
[
The authors of this paper have conducted a number of investigations in the field under
research: for example, in the article [
Let’s start with the intersection operation . Let us formalize the notion of a class:
by a class we mean a pair K s, , where s is a functional binary relation which
associates an attribute with its meaning (from a universal domain D ), and is a
functional binary relation, which brings to conformity a method with its signature.
Therefore [
The intersection operation (of class specifications) is an operation of the form : , where: s1, 1 s2 , 2 s1 s2 , 1 2 , where is a standard set-theoretical intersection.
We will demonstrate some results concerning the structure of a partially ordered set (poset) F, , where
is a set of all the functional binary relations (on the
universal domain ), а is an ordinary set-theoretical inclusion. These results will
supplement the results of the paper [
Lemma 1. For the arbitrary functional binary relations and the following equality is true: f g ( f g) (domf domg) □
def
Proof. ■ Let us start with X domf domg . Let us use generally valid properties
of the set-theoretical restriction operation (a binary ratio on a set) (monotony,
distributivity etc.) [
Firstly, we have an inclusion dom( f g) domf domg X . Secondly, from this the next chain of equalities and inequalities follows: f g ( f g) dom( f g) ( f g) X f X g X f g .
Thus, f g ( f g) X ( f g ) (domf domg ) □ def Below is a relation of consistency: f g f X g X , where
def
X domf domg . In [
The following lemma’s corollary forms another criterion of consistency.
Corollary (the criterion of consistency of functional binary relations). Let f , g be arbitrary functional binary relations, and f g dom( f g) X , ( f g) dom( f g) X . □
Proof. ■ The proof is performed by using a Lemma 1 and inclusion dom( f g) X . It’s important to note that the second (the first) equivalence is a formal corollary of the first one (of the second one accordingly). □
As for the structure of the poset F, , there are two statements.
Statement 1. Poset
F,
is a lower semilattice, and at the same time, inff , g f g . □
The proof results from the fact that is a commutative idempotent semigroup and
from a well-known connection between such semigroups and lower semilattices (see,
e.g. [
More complete information about the poset F, is given by the following statement.
Statement 2. (the structure of poset F, ). The following statements are true: 1. The empty function f is the smallest element (“a bottom”) def X domf domg .
2. The largest element in poset F,
exists if and only if the universe D is singleton 3. The infimum exists for any nonempty set F and inf F f F f 4. The supremum of the set F exists if and only if in the case when the set F is restricted, and supF f F f
6. Poset F, is a relatively complete poset and a complete (upper) semilattice □ Let’s proceed to the substantial interpretation of above results.
The operation constructs a new class which will be basic (paternal) for classes arguments. This intersection can also be empty, in this case we will get a special empty class.
As the relation on the specifications is component wise ( s, s, s s ) , all properties of the relation (statements 1, 2) can be lifted to the relation . The corresponding formulations are obvious and thereby are omitted. 3
The model of intersection operation of class specifications has been examined. This operation has been specified as set-theoretical intersection. The specification f g has been interpreted as the largest total part of f and g , that is, the specification from which specifications-arguments can be obtained by inheritance (in other words, the result specification is the specification of a paternal class). The conditions for nonempty (equivalent, empty) intersection have been examined.
As for formal results, natural criteria of function consistency have been presented (corollary) which supplement the already known criteria; the structure of a partially ordered set of partial functions has been specified (statements 1, 2).