% $Id: XMLSchema.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
%
References
- XML Schema Part 1: Structures
internal draft: Id: structures.xml,v 1.13.1.15 1999/10/26 16:23:30 ht Exp
XMLSchema: trait
includes
XMLInfoSet,
XMLSchemaBasics,
XMLSchemaString,
XMLSchemaAttrs,
Set(Component, FiniteSet[Component] for Set[E]),
Set(Component, FiniteSet[AttrDecl] for Set[E])
TypeDefinition union of
simple: SimpleTypeDefinition,
complex: ComplexTypeDefinition
BaseDatatype union of
abInitio: AbInitio,
simple: SimpleTypeDefinition
AbInitio union of
string: StringAIT,
boolean: BooleanAIT,
real: RealAIT,
binary: BinaryAIT,
uri: URIAIT,
language: LanguageAIT,
nmtoken: NMTokenAIT,
timeinstant: TimeInstantAIT,
timeduration: TimeDurationAIT,
recurringinstant: RecurringInstantAIT
SimpleTypeDefinition tuple of
basetype: BaseDatatype
% @@others...
ComplexTypeDefinition tuple of
basetype: TypeDefinition,
contentModel: ContentModel,
attrDecls: FiniteSet[AttrDecl]
%@@others...
ComplexRTypeDefinition tuple of %@@subtype of above??
contentType: ContentType,
attrDecls: FiniteSet[AttrDecl]
%@@others...
ContentType union of
unconstrained: Null,
emptyCM: Null,
simpleType: SimpleTypeDefinition,
richModel: ContentModel
introduces
schema_valid: ElementItem, TypeDefinition, FiniteSet[Component] → Bool
schema_valid_string: List[Char], AbInitio → Bool
schema_valid_content: List[Item], ComplexRTypeDefinition, FiniteSet[Component] → Bool
effective_stype: SimpleTypeDefinition, FiniteSet[Component]→ AbInitio
effective_ctype: ComplexTypeDefinition, FiniteSet[Component]→ ComplexRTypeDefinition
find_component: Def_or_Decl_tag, List[Char], TargetNS, FiniteSet[Component] → Component
all_white: List[Char] → Bool
asserts
∀
eii: ElementItem,
tyDef: TypeDefinition,
effectiveSchema: FiniteSet[Component]
schema_valid(eii, tyDef, effectiveSchema) =
(tag(tyDef) = simple
∧ attributes(eii) = {}
∧ filter(children(element(eii)), element) = empty
∧ schema_valid_string(asString(children(element(eii))),
effective_stype(tyDef.simple,
effectiveSchema)))
∨
(tag(tyDef) = complex
∧ schema_valid_attrs(attributes(eii),
effective_ctype(tyDef.complex,
effectiveSchema).attrDecls,
effectiveSchema)
∧ schema_valid_content(children(element(eii)),
effective_ctype(tyDef.complex,
effectiveSchema),
effectiveSchema)
)
∀
string: List[Char],
ait: AbInitio
schema_valid_string(string,ait) =
(tag(ait) = string
∧
string_is_string(string,ait.string))
% @@ \/ (tag(ait) = boolean /\ ...) ...
∀
content: List[Item],
crt: ComplexRTypeDefinition,
effectiveSchema: FiniteSet[Component]
schema_valid_content(content,crt,effectiveSchema) =
(((tag(crt.contentType) = emptyCM)
∧ (filter(content,element) = empty)
∧ all_white(asString(content)))
∨
% @@ lots more clauses needed
true)
∀
ccs: FiniteSet[Component],
comp: Component,
localname: List[Char],
tns: TargetNS,
dd: Def_or_Decl,
ddt: Def_or_Decl_tag
(find_component(ddt,localname,tns,ccs) = comp) ⇔
(comp ∈ ccs) ∧ (comp.localname=localname) ∧ (comp.tns=tns)
∧ (comp.dex=dd) ∧ (tag(dd)=ddt)
implies
% test the simplest case
∀
eii: ElementItem,
td: TypeDefinition,
ss: FiniteSet[Component],
content: List[Item],
i: Item,
ci: CharacterItem,
std: SimpleTypeDefinition,
bt: BaseDatatype,
ait: AbInitio,
sait: StringAIT
children(element(eii))=content ∧
content={i} ∧
tag(i)=char ∧
tag(td)=simple ∧
td.simple=std ∧
std.basetype=bt ∧
tag(bt)=abInitio ∧
bt.abInitio=ait ∧
tag(ait)=string ∧
ait.string=sait ∧
tag(sait.pattern)=null ∧
tag(sait.maxLength)=null ∧
tag(sait.length)=value ∧
sait.length.value=1 ⇒ schema_valid(eii,td,ss)
% phew!
[Index]
HTML generated using lsl2html.