2- and 3-D Software Modeling
Project Description
Constraint diagrams is a visual technique,
which was introduced recently for specification of the software and other
large and complex systems. The basic idea is to express formulae of first
order predicate logic as visually appealing and intuitive drawings . The
intuitiveness of the constraint diagram language comes from it being a
natural generalization of the following classical notations, which are
part of standard mathematical education.
-
Venn-Pierce diagrams: used previously
for set-theoretical relationships. A Venn diagram contains n contours
representing n
sets. All contours must intersect in such a way that
they divide the plane into 2n zones (sometimes called
minimal regions). Any zone can be shaded to indicate that
it is empty. A non-empty collection of zones is called a region. In
a Venn-Pierce diagram, as shown in Figure 1, every region (not necessary
minimal) an X-sequence can appear denoting that region is not empty.
Figure 1. An example of
Venn-Pierce Diagram
Euler Circles: another classical method for
specifying set-theoretical relationships . Such a diagram contains contours
representing sets. As shown in Figure 3, not all contours in an Euler Circles
diagram must intersect. However, in contrast with Venn diagrams, Euler
circles do not use shading, nor the X-Sequence notation.
Figure 3. An Euler Circles
diagram
Commutative Diagrams: a notation used in mathematics
to describe properties of morphisms among mathematical structures.
Figure 4. A Commutative
diagram
For example, the semantics of commutative diagram
of Figure 4 is that " xÎ
V1
g(f(x)) = r(h(x)), or in other words, and a bit informally,
the two distinct paths leading from V1 to V4 are
equivalent for any member of V1. We say that these paths commute.
The constraint diagrams visual language
combines the notation and the ideas of Venn-Pierce diagrams, Euler circles
and commutative diagrams. An example of a constraint diagram is provided
in Figure 5.
Figure 5. A constraint
diagram giving partial specification of a library system (make legend much
smaller)
One of the constraints specified in this diagram
is the following invariant of a model of a library system. For any library
object, and any copy of that library which is on hold, that copy’s publication
must be the same as that associated with the reservation for which it is
on hold. More formally, this can be stated as the following first-order-predicate-logic
(FOPL) formula:
" xÎ
Library, " yÎ
x.collection Ç OnHold, y.onHoldFor.reserved
= y.publication
1999. This document was created by Elena
Tulchinsky as Proposal of M.Sc thesis.
All Rights Reserved.
First
Six Month Report on a STL Research Project
Researchers