.Open Records and Labeled Tuples
Records/tuples/structures/object_states are shown using the notation of Ada.
Here is a record with fields a,b,... and values xa,xb, respectively:
.As_is (a=>xa, b=>xb, ...).
The set of all objects with fields a,b,... of type
A,B, .. (respectively) is shown like this:
.As_is $ Net{ a:A, b:B, ... }.
Usually however it pays to give a name to the abstract structure
.As_is RECORD::=Net{ a:A, b:B, ... }.
This allows the structure itself to be referred to, extendded, used,
inherritted in the definitions of other structures.
The dollar sign is put infront of the name to indicate the set of
object that fit the named structure:
.As_is $ $RECORD
. Example
Class or Set:
.As_is phones::=$ Net{name:Strings, number:Strings}.
Object in `phones`:
.As_is (name=>"John Smith", number=>"714-123-5678") in phones.
Formally such a set of structures defines (and is defined by) a collection
of functions: one for each component. If X=$ Net{a:A,b:B,c:C,... } then
.As_is a in X -> A,
.As_is b in X -> B,
.As_is c in X -> C,
and if x:X then
.As_is a(x)=x.a=`the a of x`,
.As_is b(x)=x.b=`the b of x`,
.As_is c(x)=x.c=`the c of x`.
. Example - Phone numbers
(name=>"John Smith", number=>"714-123-5678").name ="John Smith"
(name=>"John Smith", number=>"714-123-5678").number ="714-123-5678"
or
name(name=>"John Smith", number=>"714-123-5678") ="John Smith"
number(name=>"John Smith",number=>"714-123-5678") ="714-123-5678"
. UML
In UML terms the field names (a,b,c,...) are role names in the
class X which would be linked to classes representing A,B,C, ...
The link normally has cardinality (0..*) at the X end.
The link must have cardinallity 1 at the other end.
The reverse role is not (usually) named in MATHS. There is a slight
abuse of notation in that the name of the role is also
used as the name of the relationship.
At the conceptual level it is best to not indicate whether the
links are aggregations, generalisations, etc. These physical
properties are not shown in the simpler MATHS model.
. Example - pairs
A>a, 2nd=>b),
So we can deduce the following formulae must also hold:
(a,b).1st=a,
(a,b).2nd=b.
1st in A>A,
2nd in A>B.
. Example - LISP functions
CAR::=1st,
CDR::=2nd,
CONS::=fun[a,b](a,b).
. Example - triples
A>**a, 2nd=>b, 3rd=>c).
. Triples and Pairs
Notice that A>****<(B>****<(B>x) in U, for any x in B, (b=>x) in U, and so on.
Further, if x:U then
.As_is type(x) = the Tag t such that (t=>x.t)=x.
Also if S is one of the sets A,B,C,....Z and s:S then
.As_is s.U = ( t=>s) in U for the 'tag' t.
. Inheritance
There is a simple notation when we want to say that one set
is a subset of another set, but with certain extra properties:
.As_is Extended_set::= Super_set with{ Extra_component and properties}
. Specifying Unique Objects
Given a structure S=$ $N, where
.As_is N=Net{a:A, b:B, c:C, ..., P, Q, R, x:=e,...}
it is not always necessary to specify all the components to determine an
unique object. For example if N=Net{ a,b:Real, a=2*b+1} then there
is exactly one object in $ $N which has a=3, namely the one with b=1. So
.As_is (a=>3, b=>1) = the n:$ $N( n.a=3 ).
A shorthand notation can be used:
.As_is the N(a=3) = (a=>3, b=>1).
In general
.As_is the N(W) = the $(N and W) = the N with(W).
whenever there is exactly one object in $(N and W).
. Constrained Structures are Subsets of Type
MATHS lets you include constraints in a structure definition. For
example the mathematical structure of a point in a plane as something
that has both Cartesian(x,y) and Polar(arg,abs) coordinates, as long
as they both refer to the same point:
POINT::=following
.Net
x,y::Real.
arg::Angle.
abs::Positive&Real.
|- abs^2=x^2+y^2.
|- tan(arg)=x/y.
.Close.Net
The symbol
.As_is |-
used above include an unproved assumption into the meaning of $POINT.
This means that
.As_is the POINT(x=>1,y=>1) = the POINT(abs=>1, arg=45.degrees).
Thus at the conceptual, logical, and mathematical level we can
document properties that must be true - without describing
any means for this to be done.
This and some other more advanced techniques makes it possible
to document the properties of real life entities.
.Close Records and Labeled Tuples
**