% $Id: xmlstruct.lsl,v 1.1 1998/01/22 03:43:49 connolly Exp $
%
% from:
% XML: From Bytes to Characters
% Bert Bos
% in XML: Principles, Tools, and Techniques
% ISBN: 1-56592-349-9
% hmmm... the hardcopy has a significant number of errors.
% a clean copy is at http://shoal.w3.org/w3j-xml/bert.html

% renamed some sorts:
% int -> Int
% char -> Char
% char[] -> CharSeq
% Identifier -> CharSeq + isIdentifier
% 2^Identifier -> CharSeqs + isIdentifier

% considering renaming:
% isNode -> isChild

xmlstruct: trait
  Node union of ch: Char, elt: XML
includes
  Set(CharSeq, CharSeqs),
  String(Char, CharSeq),
  Integer

introduces

  create: CharSeq ® XML
  setSchema : XML, URL ® XML

  getSchema : XML ® URL
% @@ + nil

  setAttribute : XML, CharSeq, CharSeq ® XML
  getAttribute : XML, CharSeq ® CharSeq
% @@CharSeq is Identifier
  getAttributes : XML ® CharSeqs
% @@CharSeq is Identifier

  addNode : XML, Node ® XML
% + error
  setNode : XML, Int, Node ® XML
% error
  getNode : XML, Int ® Node
% + nil
  nrNodes : XML ® Int
  isNode : XML, XML ® Bool
  isDescendant : XML, XML ® Bool
  isFamily : XML, XML ® Bool
  getName : XML ® CharSeq
% @@CharSeq is Identifier
  deleteAttribute : XML, CharSeq ® XML
% @@CharSeq is Identifier
  popNode : XML ® XML

  isIdentifier : CharSeq ® Bool
% @@ details about space, <, >, ...

asserts
        XML generated   by  create, setSchema, setAttribute, addNode
        XML partitioned by getName, getSchema, getAttribute, getNode

  forall S, I, I1, I2: CharSeq, U: URL, X: XML
% getSchema(create(S)) = nil

          getSchema(setSchema(X, U)) º U;


%@@ getAttribute(create(S), I) = nil

         isIdentifier(I) Þ (getAttribute(setAttribute(X, I, S), I) = S);

         (isIdentifier(I1) Ù isIdentifier(I2)) Þ
                (I1 Ø= I2 Þ getAttribute(setAttribute(X, I1, S), I2)
                                 = getAttribute(X, I2));

         getAttributes(create(S)) º {}
% getAttributes(setAttribute(X, I, S)) == getAttributes(X) \U {I}
% getAttribute(X, I) == getAttribute(setSchema(X, U), I)
% getAttributes(X) == getAttributes(setSchema(X, U))
% getSchema(X) == getSchema(setAttribute(X, I, S))


% isNode(X1, X2) <=> E N : getNode(X1, N) = X2
% isNode(X1, X2) == (getNode(X1, 0) = X2 \/ isNode(popNode(X1), X2))


% isDescendant(X1, X2) == isNode(X1, X2) | (E X3 : isNode(X3, X2) & isDescendant(X1, X3))
%@@@ isDescendant(X1, X2) == (isNode(X1, X2) \/
% isDescendantList(children(X1), X2))

%@@@ ~isDescendantList({}, X2)
%@@@ isDescendantList(X -| children, X2) == (isDescendant(X, X2) \/
% isDescendantList(children, X2))

%@@@ isFamily(X1, X2) == (X1 = X2 \/ isDescendant(X1, X2) \/
% isDescendant(X2, X1))

% isFamily(X1, X2) => addNode(X1, X2) = error
% isFamily(X1, X2) => setNode(X1, N, X2) = error
% N < 1 => setNode(X1, N, X2) = error
% N > nrNodes(X1) => setNode(X1, N, X2) = error
% N < 1 => getNode(X, N) = nil
% N > nrNodes(X) => getNode(X, N) = nil

%@@@ nrNodes(create(I)) = 0

% ~isFamily(X1, X2) => nrNodes(addNode(X1, X2)) = nrNodes(X1) + 1

% (~isFamily(X1, X2) /\ 0 < N <= nrNodes(X1)) =>
% getNode(setNode(X1, N, X2), N) = X2

%@@@@@@@@@@@

% ~isFamily(X1, X2) & N = nrNodes(X1) + 1 => getNode(addNode(X1, X2)), N) = X2

% ~isFamily(X1, X2) => getNode(X1, N) = getNode(addNode(X1, X2), N)

% ~isFamily(X1, X2) & 0 < M <= nrNodes(X1) & N <> M =>
% getNode(setNode(X1, M, X2), N) = getNode(X1, N)

% getNode(setSchema(X1, U), N) = getNode(X1, N)

% getNode(setAttribute(X1, I, S), N) = getNode(X1, N)

% ~isFamily(X1, X2) => getAttribute(addNode(X1, X2), I) =
% getAttribute(X1, I)

% ~isFamily(X1, X2) & 0 < N <= nrNodes(X1) =>
% getAttribute(setNode(X1, N, X2), I) = getAttribute(X1, I)

% ~isFamily(X1, X2) => getAttributes(addNode(X1, X1)) =
% getAttributes(X1)

% ~isFamily(X1, X2) & 0 < N <= nrNodes(X1) =>
% getAttributes(setNode(X1, N, X2)) = getAttributes(X1)

% ~isFamily(X1, X2) => getSchema(addNode(X1, X2)) =
% getSchema(X1)

% ~isFamily(X1, X2) & 0 < N <= nrNodes(X1) =>
% getSchema(setNode(X2, N, X2)) = getSchema(X1)

% getName(create(I)) = I

% getName(setSchema(X, U)) = getName(X)

% getName(setAttribute(X, I, S)) = getName(X)

% ~isFamily(X1, X2) => getName(addNode(X1, X2)) = getName(X1)

% ~isFamily(X1, X2) & 0 < N <= nrNodes(X1) => getName(setNode(X1, N, X2)) = getName(X1)
% deleteAttribute(create(I1), I2) = create(I1)

% getSchema(deleteAttribute(X, I)) = getSchema(X)

% getAttribute(deleteAttribute(X, I), I) = nil

% getAttributes(deleteAttribute(X, I)) = getAttributes(X) \ {I}

% getNode(deleteAttribute(X, I), N) = getNode(X, N)

% getName(deleteAttribute(X, I)) = getName(X)
% popNode(create(I)) = create(I)

% ~isFamily(X1, X2) => popNode(addNode(X1, X2)) = X1

% ~isFamily(X1, X2) & 0 < N < nrNodes(X1) => popNode(setNode(X1, N, X2)) = setNode(popNode(X1), N, X2)

% ~isFamily(X1, X2) & N = nrNodes(X1) => popNode(setNode(X1, N, X2)) = popNode(X1)

% nrNodes(X) > 0 => nrNodes(popNode(X)) = nrNodes(X) - 1

% N < nrNodes(X) => getNode(popNode(X), N) = getNode(X, N)

% getSchema(popNode(X)) = getSchema(X)

% getAttribute(popNode(X), I) = getAttribute(X)

% getAttributes(popNode(X)) = getAttributes(X)

% getName(popNode(X)) = getName(X)

%implies
% converts isSchema exempting forall S: Identifier getschema(create(S))

[Index]

HTML generated using lsl2html.