specification [NAME, ATTRIBUTE_NAME, CONTENTS, char] | Node,Arc,IsA,T: NAME % [ATTRIBUTE_VALUE] ATTRIBUTE_VALUE ::= pos_int << N >> | int << Z >> | string << seq char >> | attribute_value: ATTRIBUTE_VALUE % generic value
ATTR_FLAGS ::= CONSTANT | PRIVATE ---ATTRIBUTE------------------------------------------------------------- | Name: ATTRIBUTE_NAME; | Value: ATTRIBUTE_VALUE; | Priority: Z; | Flags: P ATTR_FLAGS; -------------------------------------------------------------------------MakeAttribute is a convenient function to create a new attribute. [Implementation: declaration]
| MakeAttribute: ATTRIBUTE_NAME & ATTRIBUTE_VALUE & Z & P ATTR_FLAGS | --> ATTRIBUTE |----------- | MakeAttribute = (lambda n:ATTRIBUTE_NAME; v:ATTRIBUTE_VALUE; p:Z; f:P ATTR_FLAGS @ | (mu a:ATTRIBUTE | a.Name=n /\ a.Value=v /\ a.Priority=p /\ a.Flags=f))
[VALIDATOR] ---COMPONENT0------------------------------------------------------------ | Name: NAME; | Level: Z; | Attributes: P ATTRIBUTE; | Constraints: P VALIDATOR; -------------------------------------------------------------------------[Implementation: declaration] NODE0 is node-specific extension to COMPONENT0. It has some unspecified contents.
---NODE0----------------------------------------------------------------- | Contents: CONTENTS; -------------------------------------------------------------------------Arcs take a little more work to specify than nodes. Arcs are very general in this specification: they have an arbitrary arity (they need not be binary), and they may terminate at an arbitrary component (either nodes or other arcs). Since COMPONENT has not yet been completely defined it is temporarily pre-declared as a given set.
[COMPONENT]The terminals of an arc have direction besides a reference to the archor component. All arcs must have at least one terminal. [Implementation: declaration and code]
DIRECTION ::= FROM | TO | BIDIRECT | NONE ---TERMINAL-------------------------------------------------------------- | Anchor: COMPONENT; | Direction: DIRECTION; -------------------------------------------------------------------------ARC0 is the extension of COMPONENT0 for arcs. [Implementation: declaration and code]
---ARC0------------------------------------------------------------------ | Terminals: seq TERMINAL; |--------------- | #Terminals > 0 -------------------------------------------------------------------------Finally, the parts can be brought together to define a component. The basic components of a graph are nodes and arcs. A COMPONENT is the base, COMPONENT0 (name, level, and attributes) together with the NODE0 or ARC0 extension.
COMPONENT_TYPES ::= node << NODE0 >> | arc << ARC0 >> | isa_arc << ARC0 >> ---COMPONENT------------------------------------------------------------- | COMPONENT0; | Role:COMPONENT_TYPES; |------------- | COMPONENT0; ------------------------------------------------------------------------- | MakeTerminal: COMPONENT & DIRECTION --> TERMINAL |--------------- | MakeTerminal = (lambda c:COMPONENT; d:DIRECTION @ | (mu t:TERMINAL | t.Anchor=c /\ t.Direction=d))NODE_COMPONENT, ARC_COMPONENT and ISA_COMPONENT are simply a conveniences to refer to arcs and nodes.
NODE_COMPONENT =^= [COMPONENT | Role in ran node] ARC_COMPONENT =^= [COMPONENT | Role in ran arc] ISA_COMPONENT =^= [COMPONENT | Role in ran isa_arc]The functions Terminal and TerminalDir are conveniences to extract individual terminals and direction of individual terminals from arcs.
| NULLCOMPONENT: COMPONENT | GetTerminal: ARC_COMPONENT & N +-> COMPONENT; | GetTerminalDir: ARC_COMPONENT & N +-> DIRECTION; |-------------- | forall a:ARC_COMPONENT; n:N | n <= #(arc~(a.Role)).Terminals @ | GetTerminal(a,n) = (((arc~(a.Role)).Terminals)(n)).Anchor /\ | GetTerminalDir(a,n) = (((arc~(a.Role)).Terminals)(n)).Direction;
The parts of a graph (nodes, arcs, and isa arcs) are themselves type objects in this theory. A node is called "Node", etc. The three components all reside (uniquely) in highest type level. A graph always contains the basic components node, arc, and isa.
Within a graph, we can describe the traditional subtyping relations. Here the relation parentof refers to only immediate parents, while the relation ancestorof is the normal proper subtype relation. isa is as expected: just the same as ancestorof except that identity is included. Note that the direction of the isa relation is the reverse of the other two!
There are several constraints on a TYPED_GRAPH:
%% inrel parentof %% inrel ancestorof %% inrel isa ---GRAPH0--------------------------------------------------------------- | Contents: P COMPONENT; | TOP: COMPONENT; | NODE: NODE_COMPONENT; | ARC: ARC_COMPONENT; | ISA: ISA_COMPONENT; | Level1Objects: P COMPONENT; | _ parentof _ : COMPONENT <-> COMPONENT; | _ ancestorof _ : COMPONENT <-> COMPONENT; | _ isa _ : COMPONENT <-> COMPONENT; | % these next 3 awkwardly shadow the above due to syntax constraints | parentof0 : COMPONENT <-> COMPONENT; | ancestorof0 : COMPONENT <-> COMPONENT; | isa0 : COMPONENT <-> COMPONENT; |-------------- | Level1Objects = {TOP, NODE, ARC, ISA}; | forall c,p:Contents @ p->c in parentof0 <=> p parentof c; | forall c,p:Contents @ p->c in ancestorof0 <=> p ancestorof c; | forall c,p:Contents @ c->p in isa0 <=> c isa p; | Level1Objects subseteq Contents; | | % _ parentof _ : a little complicated because we need a special case | % for ISA_COMPONENTs to prevent endless recursion of isa's | (forall p,c:Contents | p /= ISA @ | p parentof c <=> (exists a:ISA_COMPONENT | a in Contents @ | GetTerminal(a,2) = p /\ GetTerminal(a,1) = c)) | /\ | (forall p,c:Contents | p = ISA @ | p parentof c <=> (c.Role in ran isa_arc /\ p /= c /\ | not (exists a:ISA_COMPONENT | a in Contents @ | GetTerminal(a,2) = p /\ GetTerminal(a,1) = c))); | | % _ancestorof _ | forall c1,c2:Contents @ | c1 ancestorof c2 <=> (c1,c2) in ( _ parentof _ )^*; | | % _ isa _ | forall p,c:Contents @ c isa p <=> ((p = c) \/ (p ancestorof c)); | | % details of the level 1 components | TOP.Name = T; | TOP.Level = 1; | | NODE.Name = Node; | NODE.Level = 1; | NODE.Role in ran node; | | ARC.Name = Arc; | ARC.Level = 1; | #(arc~(ARC.Role)).Terminals = 0; | | ISA.Name = IsA; | ISA.Level = 1; | GetTerminal(ISA,1) = TOP; | GetTerminal(ISA,2) = TOP; | | % the type hierarchy for the level 1 components | NODE isa TOP; | ARC isa TOP; | ISA isa ARC; | | % The only level 1 objects are TOP, NODE, ARC, and ISA and their | % isa arcs that define the type hierarchy | #{c:COMPONENT | c.Level = 1} = 7; | | % there are no cycles over the isa relationship | forall c:Contents @ not (c ancestorof c); | | % everything is a NODE or ARC, but only one of these | forall c:Contents @ | (c isa NODE \/ c isa ARC) /\ | (c isa NODE) => not (c isa ARC) /\ | (c isa ARC ) => not (c isa NODE); | ------------------------------------------------------------------------
VRES ::= PASS | FAIL VALIDATOR == COMPONENT & COMPONENT & GRAPH0 --> VRESIn the follwing, we define a few VALIDATORS that we will need shortly.
No arc may refer to itself. This rule will be added to the definition of an ARC. [Implementation: code]
| NoSelfReference: VALIDATOR |-------------- | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | NoSelfReference(apply,owner,g) = | if (forall t:second(| (arc~(apply.Role)).Terminals |) @ | apply /= t.Anchor) | then PASS | else FAILThe following 3 VALIDATOR templates restricts the arity of an arc. They are actually a functions that takes a positive integer argument and return a VALIDATOR that restricts the arity to be equal-to/greater-than/less-than the value of the argument. This can be easily implemented as a C++ function object (with state -- the argument). [Implementation: code]
| ArityEquals: N1 --> VALIDATOR |--------------- | forall n: N1 @ | ArityEquals(n) = (mu v:VALIDATOR | | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | v(apply,owner,g) = | if (#((arc~(apply.Role)).Terminals) = n) | then PASS | else FAIL)The Directed VALIDATOR specifies a binary from-to arc. [Implementation: code]
| Directed: VALIDATOR |-------------- | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | Directed(apply,owner,g) = | if (ArityEquals(2)(apply,owner,g)=PASS /\ | GetTerminalDir(apply,1) = FROM /\ | GetTerminalDir(apply,2) = TO) | then PASS | else FAILThe Upward VALIDATOR is a specialization of the Directed VALIDATOR that must be from an object at a level lower or equal to the the level of the to side. Also, the level of the isa arc itself must be the same as that of the from side. [Implementation: code]
| Upward: VALIDATOR |-------------- | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | Upward(apply,owner,g) = | if (Directed(apply,owner,g)=PASS /\ | (GetTerminal(apply,1)).Level >= (GetTerminal(apply,2)).Level /\ | apply.Level <= (GetTerminal(apply,1)).Level) | then PASS | else FAILAn arc cannot refer to anything outside the graph it is contained in. This validator is related to the NoDanglingTerminals validator, but this one allows dangling terminals and explicity checks for graph membership (NoDanglingTerminals doesn't). [Implementation: code]
| ConfinedToGraph: VALIDATOR |-------------- | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | ConfinedToGraph(apply,owner,g) = | if (forall i:N | i<=#(arc~(apply.Role)).Terminals @ | GetTerminal(apply,i) in (g.Contents || {NULLCOMPONENT})) | then PASS | else FAILA component cannot override a CONSTANT attribute. [Implementation: code]
| NoConstAttrOverrides: VALIDATOR |-------------- | forall apply, owner: COMPONENT @ forall g: GRAPH0 @ | NoConstAttrOverrides(apply,owner,g) = | if (forall a:apply.Attributes @ | not (exists c2:g.Contents | c2->apply in g.ancestorof0 @ | forall a2:c2.Attributes | a2.Name = a.Name @ CONSTANT in a2.Flags)) | then PASS | else FAILArcs must conform to their parents' arcs; that is, the child's arity must be greater than or equal to the arity of the parent, and all terminating objects in the child must be sub-types (or equal) of the corresponding (and non-missing) types of the parent's terminating objects. [Implementation: code]
| ArcConformance: VALIDATOR |-------------- | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | ArcConformance(apply,owner,g) = | if (forall c2:ARC_COMPONENT | c2 in g.Contents /\ c2->apply in g.ancestorof0 @ | % subtypes must have equal or more terminals | #(arc~(c2.Role)).Terminals <= #(arc~(apply.Role)).Terminals /\ | % subtypes must type-conform at each terminal | (forall i:Z | i<=#(arc~(c2.Role)).Terminals @ | GetTerminal(apply,i)->GetTerminal(c2,i) in g.isa0)) | then PASS | else FAILArcs between arcs are not allowed (except ARC itself and all ISA arcs). Can be used at the ARC level to force first order graphs. [Implementation: code]
| NoArcBtwnArcs: VALIDATOR |-------------- | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | NoArcBtwnArcs(apply,owner,g) = | if ((apply->g.ARC in g.isa0 /\ apply /= g.ARC /\ not(apply->g.ISA in g.isa0)) => (forall t:TERMINAL | | t in ran (arc~(apply.Role)).Terminals @ t.Anchor->g.NODE in g.isa0)) | then PASS | else FAILAn arc with the NoDanglingTerminals contraint must have all its terminals linked to a valid object in the graph (none must be uninstantiated or "dangling"). This constraint naturally applies to all isa arcs. Note that this is related to the ConfinedToGraph validator, ConfinedToGraph allows dangling terminals while this one doesn't, and also doesn't explicitly check for membership in the graph. [Implementation: code]
| NoDanglingTerminals: VALIDATOR |-------------- | forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @ | NoDanglingTerminals(apply,owner,g) = | if (forall i:N | i<=#(arc~(apply.Role)).Terminals @ | GetTerminal(apply,i) in g.Contents) | then PASS | else FAIL
---TYPED_GRAPH----------------------------------------------------------- | GRAPH0; |------------- | % T restrictions | {NoConstAttrOverrides} subseteq TOP.Constraints; | | % arc restrictions | {NoSelfReference, ConfinedToGraph, ArcConformance} | subseteq ARC.Constraints; | | % an isa arc is binary upward-directed arc (recall that ISA isa ARC, and | % "inherits" its constraints) | {Upward, NoDanglingTerminals} subseteq ISA.Constraints; | | % all components satisfy their constraints | exists g:GRAPH0 | g.Contents = Contents @ | forall c:g.Contents @ | forall c2:g.Contents | c isa c2 @ forall v:VALIDATOR | v in c2.Constraints @ | v(c,c2,g) = PASS; | --------------------------------------------------------------------------The following is a consistency corrollary of the above TYPED_GRAPH schema and can easily be proved from it. Every component is the same top-level type as all of its supertypes.
forall g:TYPED_GRAPH @ forall c1,c2:g.Contents | c1->c2 in g.isa0 @ c1->g.NODE in g.isa0 <=> c2->g.NODE in g.isa0 /\ c1->g.ARC in g.isa0 <=> c2->g.ARC in g.isa0 /\ c1->g.ISA in g.isa0 <=> c2->g.ISA in g.isa0
%% state-schema FIRST_ORDER_TYPED_GRAPH FIRST_ORDER_TYPED_GRAPH =^= [TYPED_GRAPH | {NoArcBtwnArcs} subset ARC.Constraints ]
GETATTR_RESULT ::= Attr<The getValue function is similar to the above function, but simply returns a value if one can be found.> | NULLr | getAttr: TYPED_GRAPH & COMPONENT & ATTRIBUTE_NAME --> GETATTR_RESULT |-------------- | forall g:TYPED_GRAPH; c:COMPONENT; a:ATTRIBUTE_NAME | c in g.Contents @ | getAttr(g,c,a) = | if a in {a1:ATTRIBUTE_NAME | exists at:c.Attributes @ a1 = at.Name} | % c actually has the attribute | then (mu x:c.Attributes | (a = x.Name)) | else if {x:GETATTR_RESULT | forall c2:g.Contents | c2->c in g.parentof0 @ | x=getAttr(g,c2,a)} = {} | % attribute not found | then NULLr | % attribute found in one of the ancestors | else (mu x:ATTRIBUTE | forall c2:g.Contents | c2->c in g.parentof0 /\ | (exists y:ATTRIBUTE @ y=Attr~(getAttr(g,c2,a))) @ | exists y:ATTRIBUTE | y=Attr~(getAttr(g,c2,a)) @ | forall c3:g.Contents | c3->c in g.parentof0 /\ | (exists z:ATTRIBUTE @ z=Attr~(getAttr(g,c3,a))) /\ | (not (c3->c2 in g.ancestorof0)) @ | exists z:ATTRIBUTE | z=Attr~(getAttr(g,c3,a)) @ | y.Priority<=z.Priority /\ x=y)
GETVALUE_RESULT ::= Val<setAttr takes a component and an attribute and merely adds the attribute to the components set of attributes, replacing any attributes who's name might have matched.> | NULLv | getValue : TYPED_GRAPH & COMPONENT & ATTRIBUTE_NAME --> GETVALUE_RESULT |--------------- | forall g:TYPED_GRAPH; c:COMPONENT; a:ATTRIBUTE_NAME | c in g.Contents @ | getValue(g,c,a) = if getAttr(g,c,a)=NULLr | then NULLv | else (Attr~(getAttr(g,c,a))).Value
---setAttr---------------------------------------------------------------- | Delta TYPED_GRAPH; | c?: COMPONENT; | attr?: ATTRIBUTE |--------------- | c? in Contents; | Contents' = (Contents \ {c?}) || {(mu c2:Contents | | c2.Name = c?.Name /\ | c2.Level = c?.Level /\ | c2.Role = c?.Role /\ | c2.Attributes = (c?.Attributes \ | {a:c?.Attributes | a.Name = attr?.Name}) || | {attr?})} --------------------------------------------------------------------------
---ADD_NODE--------------------------------------------------------------- | Delta TYPED_GRAPH; | node?: NODE_COMPONENT; | type?: NODE_COMPONENT |--------------- | TYPED_GRAPH'; | type? in Contents; | not (node? in Level1Objects); | Contents' = Contents || {node?, (mu a:ISA_COMPONENT | | GetTerminal(a,1)=node? /\ GetTerminal(a,2)=type?) }; --------------------------------------------------------------------------Note that due to the invarients on the graph, the node cannot have any non-ISA arcs in the graph that refering to it immediate after its insertion. Note also that, by virtue of the definition of NODE_COMPONENT, the new node isa NODE (and therefore there exists an ISA link from the new node to NODE.
Its just as simple to add a new arc:
---ADD_ARC---------------------------------------------------------------- | Delta TYPED_GRAPH; | arc?: ARC_COMPONENT; | type?: ARC_COMPONENT |--------------- | TYPED_GRAPH'; | type? in Contents; | not(arc? isa ISA); | not(arc? in Level1Objects); | Contents' = Contents || {arc?, (mu a:ISA_COMPONENT | | GetTerminal(a,1)=arc? /\ GetTerminal(a,2)=type?)}; --------------------------------------------------------------------------But note that note that there is more going on here than meets the eye. Because of the constraints on a typed graph, the arc must refer only to nodes that are already members of the graph contents.
It must also be possible to change the type of node or link:
---CHANGE_TYPE------------------------------------------------------------ | Delta TYPED_GRAPH; | c?: COMPONENT; | newType?: COMPONENT |--------------- | TYPED_GRAPH'; | (c? isa NODE /\ newType? isa NODE) \/ | (c? isa ARC /\ newType? isa ARC ) \/ | (c? isa ISA /\ newType? isa ISA ); | c? in (Contents \ Level1Objects); | newType? in Contents; | Contents' = (Contents \ {a:ISA_COMPONENT | GetTerminal(a,1) = c?}) || | {(mu a:COMPONENT | GetTerminal(a,1)=c? /\ GetTerminal(a,2)=newType?)}; --------------------------------------------------------------------------Removing any component from a graph entails removing all arcs (including isa arcs) that reference the removed node. One problem is that if the removed node was the type of some existing component, then the "lower" components will be left with dangling isa chains. This is prevented by disallowing it in precondition.
---REMOVE----------------------------------------------------------------- | Delta TYPED_GRAPH; | c?: COMPONENT; |--------------- | TYPED_GRAPH'; | c? in (Contents \ Level1Objects); | not (exists c2:Contents @ c2 isa c?); | Contents' = Contents \ | ({c?} || {a:ARC_COMPONENT | (exists i:N @ GetTerminal(a,i)=c?)}) --------------------------------------------------------------------------
end specification