kremer@cpsc.ucalgary.ca

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

Runtime 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

	include {Dexter~2.htm}

GivenSets


	[IID]

	[BASE_INSTANTIATION, LINK_MARKER]

INSTANTIATION


	---INSTANTIATION--------------------------------------------------------
	| base: BASE_INSTANTIATION;
	| links: seq LINK_MARKER;
	| linkAnchor: LINK_MARKER --> ANCHOR_ID
	|----------------------
	| dom linkAnchor = ran links
	------------------------------------------------------------------------

OPERATION


	OPERATION ::= OPEN | CLOSE | PRESENT | UNPRESENT
		    | CREATE | EDIT | SAVE | DELETE

Session


	---SESSION--------------------------------------------------------------
	| H: HYPERTEXT;
	| history: seq OPERATION;
	| instants: IID >+> (INSTANTIATION & UID);
	| instantiator: UID & PRESENT_SPEC --> INSTANTIATION;
	| realizer: INSTANTIATION --> COMPONENT;
	| runTimeResolver: COMPONENT_SPEC +-> UID
	|---------------------
	| head(history) = OPEN;
	| forall uid: UID; ps: PRESENT_SPEC | uid in dom H.accessor @
	|	realizer(instantiator(uid,ps)) = H.accessor(uid) /\
	|	H.resolver subseteq runTimeResolver
	------------------------------------------------------------------------

	---Delta SESSION -------------------------------------------------------
	| SESSION;
	| SESSION'
	|---------------------
	| #history' = #history + 1;
	| instantiator' = instantiator;
	| realizer' = realizer
	------------------------------------------------------------------------

	---openSession----------------------------------------------------------
	| SESSION;
	| hypertext?: HYPERTEXT
	|---------------------
	| H = hypertext?;
	| history = <>;
	| instants = {}
	------------------------------------------------------------------------

Component Operations


	| openComponents: SESSION & F(SPECIFIER & PRESENT_SPEC) --> SESSION
	|---------------------
	| forall S: SESSION; specs: F(SPECIFIER & PRESENT_SPEC) @
	|	exists S': SESSION; iids: F IID;
	|			newInstants: IID >+> (INSTANTIATION & UID) |
	|		S'.H = S.H /\
	|		S'.runTimeResolver = S.runTimeResolver /\
	|		S'.history = S.history ^ <> /\
	|		S'.instants = S.instants += newInstants /\
	|		#iids = #specs /\ iids && dom S. instants = {} /\
	|		dom newInstants = iids /\
	|		(forall s: specs @
	|			exists iid: iids; uid: UID; cs:COMPONENT_SPEC;
	|				ps: PRESENT_SPEC; inst: INSTANTIATION |
	|			cs = (first(s)).componentSpec /\
	|			ps = second(s) /\
	|			uid = S.runTimeResolver(cs) /\
	|			inst = S.instantiator(uid,ps) @
	|			newInstants(iid) = (inst,uid)) @
	|		openComponents(S,specs) = S'

	---presentComponent-----------------------------------------------------
	| Delta SESSION;
	| spec?: SPECIFIER;
	| presentSpec?: PRESENT_SPEC
	|------------------------
	| theta SESSION' = openComponents(theta SESSION,{(spec?,presentSpec?)})
	------------------------------------------------------------------------

followLink


	---followLink-----------------------------------------------------------
	| Delta SESSION;
	| iid?: IID;
	| linkMarker?: LINK_MARKER
	|------------------------
	| exists aid: ANCHOR_ID; links: F LinkComp; 
	|				specs: F(SPECIFIER & PRESENT_SPEC) |
	|	aid = (first(instants(iid?))).linkAnchor(linkMarker?) /\
	|	links = H.accessor (| LinksToAnchor (H, 
	|				second (instants(iid?)),aid) |) /\
	|	first (| specs |) = {s: SPECIFIER | exists linkc: LinkComp |
	|		linkc in links @ s in ran(link~(base(linkc))).specifiers} /\
	|	(forall s: specs @ (first(s)).direction = TO /\
	|			second(s) = (first(s)).presentSpec) @
	|		theta SESSION' = openComponents(theta SESSION,specs)
	------------------------------------------------------------------------

newComponent


	---newComponent---------------------------------------------------------
	| Delta SESSION;
	| component: COMPONENT;
	| baseComp?: BASE_COMPONENT;
	| ps?: PRESENT_SPEC;
	| presentSpec?: PRESENT_SPEC
	|-----------------------
	| history' = history ^ <>;
	| (H',component) = CreateNewComponent(H,baseComp?,ps?);
	| exists uid: UID; inst: INSTANTIATION; iid: IID |
	|	iid notin dom instants @
	|		inst = instantiator(uid,presentSpec?) /\
	|		uid = H'.accessor~(component) /\
	|		instants' = instants += {iid -> (inst,uid)}
	------------------------------------------------------------------------

unPresent


	---unPresent------------------------------------------------------------
	| Delta SESSION;
	| iid?: IID
	|----------------------
	| H' = H;
	| history' = history ^ <>;
	| instants' = {iid?} <+ instants
	------------------------------------------------------------------------

editInstantiation


	---editInstantiation----------------------------------------------------
	| Delta SESSION;
	| instantiation?: INSTANTIATION;
	| iid?: IID
	|----------------------
	| H' = H;
	| history' = history ^ <>;
	| iid? in dom instants;
	| instants' = instants +=
	|	{iid? -> (instantiation?,second(instants(iid?)))}
	------------------------------------------------------------------------

realizeEdits


	---realizeEdits---------------------------------------------------------
	| Delta SESSION;
	| iid?: IID
	|----------------------
	| history' = history ^ <>;
	| instants' = instants;
	| exists c: COMPONENT; inst: INSTANTIATION; uid: UID |
	|	inst = first(instants(iid?)) /\
	|	uid = second(instants(iid?)) /\
	|	c = realizer(inst) @
	|		H' = ModifyComponent(H,uid,c)
	------------------------------------------------------------------------

deleteComponent


	---deleteComponent------------------------------------------------------
	| Delta SESSION;
	| iid?: IID
	|----------------------
	| history' = history ^ <>;
	| iid? in dom instants;
	| exists uid: UID | uid = second(instants(iid?)) @
	|	H' = DeleteComponent(H,uid) /\
	|	instants' = {iid?} <+ instants
	------------------------------------------------------------------------

closeSession


	---closeSession---------------------------------------------------------
	| Delta SESSION
	|----------------------
	| H' = H;
	| history' = history ^ <>;
	| instants' = {}
	------------------------------------------------------------------------

READ_ONLY_SESSION


	---READ_ONLY_SESSION----------------------------------------------------
	| Delta SESSION
	|----------------------
	| {SAVE,CREATE,DELETE} && ran history = {}
	------------------------------------------------------------------------

	end specification
up to index, kremer@cpsc.ucalgary.ca