% $Id: WadlerProps.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%

WadlerProps: trait
    includes
        XPathWadler

    introduces
        M': Pattern, Node → Bool
% Wadler writes Pattern x Node -> Bool, but then uses
% it as a higher-order function. odd.

    asserts forall p, p1: Pattern,
                   x, x1, x2: Node,
                   s: String

        M'(p, x) = ∃ x1 (x1 ∈ (parent*)[x]
                           ∧ x ∈ S(p)[x1]);

    implies forall p, p1: Pattern, x: Node, s: String

%@@ p not containing id(p), ancestor(p), ancestor-or-self(p), ..
%M(p, x) = M'(p, x);

        p = !p1 ∨ p = id(s) ⇒
            S(p)[x] = S(p)[root(x)];

% p @@ not containing /p, id(s), ancestor(p), anc-or-self(p), ..
%S(p)[x] \subseteq (subnodes\superstar)[x];

%@@ save this for later...
% S(p!id(dot))[x] = S(id(p))[x];

[Index]


HTML generated using lsl2html.