kremer@cpsc.ucalgary.ca

Dexter1: Z Specification of a variation of the Dexter Hypertext Reference Model

Storage Layer

This specification is a variation of the one given in:
Halasz, F., Schwartz, M. "The Dexter Hypertext Reference Model." NIST Hypertext Standardization Workshop, Gaithersburg, MD. January 16-18, 1990.
WARNING: Work in progress

Page Contents


	specification

GivenSets


	[UID]

	[COMPONENT_SPEC, PRESENT_SPEC]

	DIRECTION ::= FROM | TO | BIDIRECT | NONE

	[ANCHOR_ID, ANCHOR_VALUE]

	include {types~1.htm}

ANCHOR


	ANCHOR == ANCHOR_ID & ANCHOR_VALUE

Specifiers


	---SPECIFIER------------------------------------------------------------
	| componentSpec: COMPONENT_SPEC;
	| anchorSpec: ANCHOR_ID;
	| presentSpec: PRESENT_SPEC;
	| direction: DIRECTION;
	------------------------------------------------------------------------

Links


	---LINK-----------------------------------------------------------------
	| specifiers: seq SPECIFIER
	|------------
	| #specifiers >= 1;
	| exists s: ran specifiers @ s.direction = TO
	------------------------------------------------------------------------
Dexter1 disallows zero-ary links, but allows unary or greater links (the original Dexter insists on at least binary links).

Component Info


	[ATOM]

	[ATTRIBUTE, VALUE]


	---COMP_INFO------------------------------------------------------------
	| attributes: ATTRIBUTE +-> VALUE; 
	| anchors: seq ANCHOR;
	| presentSpec: PRESENT_SPEC;
	| % type of the link, atom or composite 
	| type: String
	|-------------
	| #anchors = #(first (| ran anchors |) ) % anchor ids are unique within
	|                                        % the component
	------------------------------------------------------------------------

	| minInfo: PRESENT_SPEC --> COMP_INFO % 
	|-------------
	| forall ps: PRESENT_SPEC @
	|	minInfo(ps) = (mu info: COMP_INFO |
	|		info.attributes = {} /\
	|		info.anchors = <<>> /\
	|		info.presentSpec = ps /\
	|		info.type = Undefined) % "Undefined" is a standard type

Base Component/Components


	BASE_COMPONENT ::= atom << ATOM >>
			|  link << LINK >>
			|  composite << seq BASE_COMPONENT >>

	---COMPONENT------------------------------------------------------------
	| compBase: BASE_COMPONENT;
	| compInfo: COMP_INFO
	------------------------------------------------------------------------

Component Helpers Functions and Predicates

The following don't really contribute to the spec, but they do make it easier to read... 

	| component: BASE_COMPONENT & COMP_INFO --> COMPONENT
	|-------------
	| component = (lambda b: BASE_COMPONENT; i: COMP_INFO @
	|	(mu c: COMPONENT |
	|		c.compBase = b /\
	|		c.compInfo = i))	

	| base: COMPONENT --> BASE_COMPONENT;
	| info: COMPONENT --> COMP_INFO
	|--------------
	| forall c: COMPONENT @
	|	base(c) = c.compBase /\
	|	info(c) = c.compInfo

	%% prerel isAtom	
	%% prerel isLink	
	%% prerel isComposite	

	| isAtom _ : P COMPONENT;
	| isLink _ : P COMPONENT;
	| isComposite _ : P COMPONENT
	|---------------
	| forall c: COMPONENT @
	|	isAtom c <=> base(c) in ran atom /\
	|	isLink c <=> base(c) in ran link /\
	|	isComposite c <=> base(c) in ran composite

	%% inrel typeConsistent

	| _ typeConsistent _ : COMPONENT <-> COMPONENT
	|----------------
	| forall c1, c2: COMPONENT @
	|	c1 typeConsistent c2 <=>
	|		(isAtom c1 /\ isAtom c2) \/
	|		(isLink c1 /\ isLink c2) \/
	|		(isComposite c1 /\ isComposite c2)

	---LinkComp-------------------------------------------------------------
	| COMPONENT
	|-----------------
	| compBase in ran link
	------------------------------------------------------------------------

	| componentSpecs: LinkComp +-> F COMPONENT_SPEC;
	| anchorSpecs: LinkComp +-> F ANCHOR_ID
	|-----------------
	| forall c: LinkComp @
	|	componentSpecs(c) = {cs: COMPONENT_SPEC |
	|		exists s: ran(link~(base(c))).specifiers @
	|			cs = s.componentSpec} /\
	|	anchorSpecs(c) = {as: ANCHOR_ID |
	|		exists s: ran(link~(base(c))).specifiers @
	|			as = s.anchorSpec}

	| attributes: COMPONENT --> (ATTRIBUTE +-> VALUE);
	| anchors: COMPONENT --> F ANCHOR
	|------------------
	| forall c: COMPONENT @
	|	attributes(c) = (info(c)).attributes /\
	|	anchors(c) = ran(info(c)).anchors

	| modifyAttribute: COMPONENT & ATTRIBUTE & VALUE --> COMPONENT
	|------------------
	| modifyAttribute = (lambda c: COMPONENT; a: ATTRIBUTE; v: VALUE @
	|	(mu c': COMPONENT | exists i, i': COMP_INFO | i = info(c) @
	|		i'.attributes = i.attributes += {a -> v} /\
	|		i'.anchors = i.anchors /\
	|		i'.presentSpec = i.presentSpec /\
	|		c' = component(base(c),i')))

	%% inrel subcomp

	| _ subcomp _ : COMPONENT <-> COMPONENT
	|------------------
	| forall c1, c2: COMPONENT @
	|	c1 subcomp c2 <=>
	|		base(c1) in ran(composite~(base(c2)))

The Hypertext Definition


	---PROTO_HYPERTEXT------------------------------------------------------
	| components: F COMPONENT;
	| resolver: COMPONENT_SPEC +-> UID;
	| accessor: UID >+> COMPONENT;
	| typeDB: TypeDB; % new!
	|---------------------
	| % All components have types that are in the type DB 
	| forall c: components @
	|   base(c) in ran link =>
	|     (exists t: LinkType | t in typeDB.LinkTypes @
	|	(info(c)).type = t.name) /\
	|   base(c) in ran atom =>
	|     (exists t: AtomType | t in typeDB.AtomTypes @
	|	(info(c)).type = t.name)
	------------------------------------------------------------------------

	| linksTo: PROTO_HYPERTEXT & UID --> F UID
	|-------------------
	| linksTo = (lambda H: PROTO_HYPERTEXT; u: UID @ {uid: UID |
	|	( exists c: LinkComp | c in H.components @
	|		uid = H.accessor~(c) /\
	|		( exists s: COMPONENT_SPEC |
	|			s in componentSpecs(c) @
	|				u = H.resolver(s)))})


	---HYPERTEXT------------------------------------------------------------
	| PROTO_HYPERTEXT
	|-------------------
	| forall c: components @ c in ran accessor;
	| ran resolver = dom accessor;
	| forall c: components @ (c,c) notin ( _ subcomp _ )^*;
	| forall c: components @ exists lids: F UID |
	|	lids = linksTo(theta PROTO_HYPERTEXT, accessor~(c)) @
	|		first (| anchors(c) |) = 
	|		Union((anchorSpecs <: accessor) (| lids |) );
	| 
	| % all links must refer only to nodes of the type allowed by the link type
	| forall l: LinkComp | l in ran accessor @
	|   exists t: LinkType | t.name = (info(l)).type @
	|     ((t.arity=0) \/ (#((link~(base(l))).specifiers) <= t.arity)) /\
	|     (forall c: components | accessor~(c) in 
	|			  linksTo(theta PROTO_HYPERTEXT,accessor~(l)) @
	|	exists i:N | (exists s: SPECIFIER @
	|	  accessor(resolver(s.componentSpec)) = c /\
	|				i = (link~(base(l))).specifiers~(s)) @
	|	    ((info(c)).type -> (t.constraints(i)).aType) in
	|						( typeDB.ATSubtype ))
	------------------------------------------------------------------------

Adding New Components


	| createComponent: HYPERTEXT & COMPONENT --> HYPERTEXT
	|-------------------
	| forall H: HYPERTEXT; c: COMPONENT @
	|	exists H': HYPERTEXT |
	|		H'.components = H.components || {c} /\
	|		(exists1 uid: UID @
	|			(exists componentSpec: COMPONENT_SPEC @
	|				H'.accessor = H.accessor || {uid -> c} /\
	|				H'.resolver = H.resolver ||
	|					{componentSpec -> uid})) @
	|						createComponent(H,c) = H'

	| createAtomicComponent: HYPERTEXT & ATOM & PRESENT_SPEC
	|						--> HYPERTEXT & COMPONENT
	|--------------------
	| forall H: HYPERTEXT; a: ATOM; ps: PRESENT_SPEC @
	|	exists c: COMPONENT | c = component(atom(a), minInfo(ps)) @
	|		createAtomicComponent(H,a,ps) =
	|			(createComponent(H,c),c)


	| NullSpec : COMPONENT_SPEC
	|-----------------------
	| forall H: HYPERTEXT @ NullSpec notin dom H.resolver


	%% prerel linkConsistent

	| linkConsistent _ : P HYPERTEXT % 
	|--------------------
	| forall H: HYPERTEXT @
	|    linkConsistent H <=>
	|	(forall l: LINK; s: SPECIFIER |
	|	    (exists cl: LinkComp | cl in H.components @
	|		l = link~(base(cl))) /\
	|	    s in ran l.specifiers @
	|	    (exists c: COMPONENT; H2: HYPERTEXT |
	|		c in H2.components @
	|		(H.accessor <: H.resolver)(s.componentSpec) = c)
	|	    \/  % this clause accounts for dangling links 
	|	    s.componentSpec = NullSpec)
Dexter1 considers a link to be consistent if it refers to an object in any hypertext (not just this one) or if one of the link terminals is explicitly left dangling. 

	| createLinkComponent: HYPERTEXT & LINK & PRESENT_SPEC
	|						--> HYPERTEXT & COMPONENT
	|--------------------
	| forall H: HYPERTEXT; l: LINK; ps: PRESENT_SPEC @
	|	exists H': HYPERTEXT; c: COMPONENT |
	|		c = component(link(l),minInfo(ps)) /\
	|		H' = createComponent(H,c) /\
	|		createLinkComponent(H,l,ps) = (H',c) @
	|			linkConsistent H'

	| createCompositeComponent: HYPERTEXT & seq BASE_COMPONENT & PRESENT_SPEC
	|						--> HYPERTEXT & COMPONENT
	|--------------------
	| forall H: HYPERTEXT; s: seq BASE_COMPONENT; ps: PRESENT_SPEC @
	|	exists newComp: COMPONENT |
	|		newComp = component(composite(s),minInfo(ps)) @
	|		createCompositeComponent(H,s,ps) =
	|			(createComponent(H,newComp),newComp) /\
	|		(forall c: COMPONENT | base(c) in ran s @
	|			c in H.components)

	| CreateNewComponent: HYPERTEXT & BASE_COMPONENT & PRESENT_SPEC
	|				--> HYPERTEXT & COMPONENT
	|--------------------
	| forall H: HYPERTEXT; bc: BASE_COMPONENT; ps: PRESENT_SPEC @
	|	((exists a: ATOM @ bc = atom(a)) => 
	|		CreateNewComponent(H,bc,ps) =
	|			createAtomicComponent(H,atom~(bc),ps)) /\
	|	((exists l: LINK @ bc = link(l)) => 
	|		CreateNewComponent(H,bc,ps) =
	|			createLinkComponent(H,link~(bc),ps)) /\
	|	((exists s: seq BASE_COMPONENT @ bc = composite(s)) => 
	|		CreateNewComponent(H,bc,ps) =
	|			createCompositeComponent(H,composite~(bc),ps))

Deleting a Component


	| DeleteComponent: HYPERTEXT & UID --> HYPERTEXT
	|--------------------
	| DeleteComponent = (lambda H: HYPERTEXT; uid: UID @
	|   (mu H': HYPERTEXT | exists uids, delUids, modUids: F UID;
	|				changes: UID >+> COMPONENT |
	|     % [1] all the effected UIDs
	|     uids = {uid} || linksTo(H,uid) /\
	|     % [2] the UIDs that should be deleted (totally empty links)
	|     delUids = {uid} || {x: UID | x in linksTo(H,uid) /\ 
	|			           (forall s: SPECIFIER; l: LinkComp |
	|	H.accessor(x) = l /\ s in ran (link~(base(l))).specifiers @
	|	  s.componentSpec = NullSpec \/ H.resolver(s.componentSpec) = uid)} /\
	|     % [3] the UIDs of LINKs that need some of their SPECIFIERs nulled
	|     modUids = uids \ delUids /\
	|     % [4] the partial function of modUids to changed COMPONENTs
	|     changes = {x: UID & COMPONENT |
	|	(exists u: UID; c',c: LinkComp | u in modUids /\ c = H.accessor(u)
	|	  @ info(c') = info(c) /\
	|	    (link~(base(c'))).specifiers = (link~(base(c))).specifiers += 
	|	      {y: N1 & SPECIFIER | (exists n: N1; s,s': SPECIFIER |
	|		n->s in (link~(base(c))).specifiers @
	|		  y = if (H.resolver(s.componentSpec) = uid) then n -> NullSpec
	|							     else n -> s')}
	|	    /\
	|	    x = u -> c')}
	|       @
	|	H'.accessor = (uids <+ H.accessor) += changes /\
	|	H'.resolver = H.resolver +> delUids /\
	|	H'.components = (H.components \ H.accessor (| uids |) ) || ran changes
	|   ))
Dexter1's DeleteComponent schema is considerably more complex than Dexter's version since instead of blindly deleteing all links that have a reference to the deleted component, Dexter1 keeps those links in the hypertext, except for the links that would be totally empty (have no reference [other than NullSpec] in any of its SPECIFIERs) after the deletion. Furthermore, Dexter1 replaces all the references (SPECIFIER.componentSpec) to the deleted component with references to NullSpec. This complex schema probably warrants explanation:

The first part of the schema is the same as Dexter's, including section [1], the set of all effected UIDs, uids. Section [2] constructs the set of all UIDs that should be deleted -- the UID that is being deleted, and all the UIDs of links that would be totally empty after the requested UID is deleted, delUids. Section [3] constructs the set of all UIDs of Link components that have to have their specifiers modified because they refer to the component being deleted, modUids; this is merely set difference between uids and delUids. Section [4] constructs the one-to-one partial function from the UIDs in modUids to modified link components that have the reference to the deleted component. The components in the range of this function replace the components in the hypertext and in its accessor function.

The remainder of the schema is similar to Dexter's version, but the changed components replace the older versions in the hypertext.

Modifying Components


	| ModifyComponent: HYPERTEXT & UID & COMPONENT --> HYPERTEXT
	|--------------------
	| forall H: HYPERTEXT; uid: UID; c': COMPONENT @
	|	exists c: COMPONENT; H': HYPERTEXT |
	|		c = H.accessor(uid) /\
	|		H'.components = H.components \ {c} || {c'} /\
	|		H'.accessor = H.accessor += {uid -> c'} /\
	|		H'.resolver = H.resolver /\
	|		info(c') = info(c) /\
	|		c typeConsistent c' /\
	|		linkConsistent H' @
	|			ModifyComponent(H,uid,c) = H'

Retrieving a Component


	| getComponent: HYPERTEXT & UID --> COMPONENT
	|--------------------
	| forall H: HYPERTEXT; uid: UID @
	|	getComponent(H,uid) = H.accessor(uid)

Attributes


	| AttributeValue: HYPERTEXT & UID & ATTRIBUTE --> VALUE
	|--------------------
	| forall H: HYPERTEXT; uid: UID; a: ATTRIBUTE @
	|	(exists c: COMPONENT | c = H.accessor(uid) @
	|		AttributeValue(H,uid,a) = attributes(c)(a))

	| SetAttributeValue: HYPERTEXT & UID & ATTRIBUTE & VALUE --> HYPERTEXT
	|--------------------
	| SetAttributeValue =
	|	(lambda H: HYPERTEXT; uid: UID; a: ATTRIBUTE; v: VALUE @
	|		(mu H': HYPERTEXT | exists c,c': COMPONENT @
	|			c = H.accessor(uid) /\
	|			c' = modifyAttribute(c,a,v) /\
	|			H'.components = H.components \ {c} || {c'} /\
	|			H'.accessor = H.accessor += {uid -> c'} /\
	|			H'.resolver = H.resolver))

	| AllAttributes: HYPERTEXT --> F ATTRIBUTE
	|--------------------
	| forall H: HYPERTEXT @
	|	AllAttributes(H) = {a: ATTRIBUTE | exists c: COMPONENT @
	|		a in dom(attributes(c))}

Anchors


	| LinksToAnchor: HYPERTEXT & UID & ANCHOR_ID --> F UID
	|--------------------
	| LinksToAnchor =
	|	(lambda H: HYPERTEXT; u: UID; aid: ANCHOR_ID @
	|		{lid: UID | exists lids: F UID |
	|			lids = linksTo(H,u) /\ lid in lids @
	|			aid in (anchorSpecs <: H.accessor)(lid)})

	end specification
up to index, forward to type DB spec
kremer@cpsc.ucalgary.ca