Z Specification of the Dexter Hypertext Reference Model

Storage Layer

This specification is 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

GivenSets
- UID, COMPONENT_SPEC, PRESENT_SPEC, DIRECTION, ANCHOR_ID, ANCHOR_VALUE
Anchors
- ANCHOR
Specifiers
- SPECIFIER
Links
- LINK
Component Info
- ATOM, ATTRIBUTE, VALUE (given sets)
- COMP_INFO
- minInfo
Base Component/Components
- BASE_COMPONENT
- COMPONENT
Component Helper Functions and Predicates
- component
- base, info
- isAtom, isLink, isComposite
- typeConsistent
- LinkComp
- componentSpecs, anchoSpecs
- attributes, anchors
- modifyAttribute
- subcomp
The Hypertext Definition
- PROTO_HYPERTEXT
- linksTo
- HYPERTEXT
Adding New Components
- createComponent
- createAtomicComponent
- linkConsistent
- createLinkComponent
- createCompositeComponent
- CreateNewComponent
Deleting a Component
- DeleteComponent
Modifying Components
- ModifyComponent
Retrieving a Component
- getComponent
Attributes
- AttributeValue
- SetAttributeValue
- AllAttributes
Anchors
- LinksToAnchor


	specification

GivenSets


	[UID]

	[COMPONENT_SPEC, PRESENT_SPEC]

	DIRECTION ::= FROM | TO | BIDIRECT | NONE

	[ANCHOR_ID, ANCHOR_VALUE]

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 >= 2;
	| exists s: ran specifiers @ s.direction = TO
	------------------------------------------------------------------------

Component Info


	[ATOM]

	[ATTRIBUTE, VALUE]

	---COMP_INFO------------------------------------------------------------
	| attributes: ATTRIBUTE +-> VALUE;
	| anchors: seq ANCHOR;
	| presentSpec: PRESENT_SPEC
	|-------------
	| #anchors = #(first (| ran anchors |) )
	------------------------------------------------------------------------

	| minInfo: PRESENT_SPEC --> COMP_INFO
	|-------------
	| forall ps: PRESENT_SPEC @
	|	minInfo(ps) = (mu info: COMP_INFO |
	|		info.attributes = {} /\
	|		info.anchors = <<>> /\
	|		info.presentSpec = ps)

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
	------------------------------------------------------------------------

	| 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 |) )
	------------------------------------------------------------------------

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)

	%% 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 | c in H.components @
	|				(H.accessor <: H.resolver)(s.componentSpec) = c))

	| 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: F UID |
	|		uids = {uid} || linksTo(H,uid) @
	|			H'.components = H.components \ H.accessor (| uids |) /\
	|			H'.accessor = uids <+ H.accessor /\
	|			H'.resolver = H.resolver +> uids))

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 Runtime Layer

kremer@cpsc.ucalgary.ca