% $Id: XMLSchemaString.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
XMLSchemaString: trait
includes
XMLInfoSet,
Integer,
RegExp(Char for Symbol, List[Char] for String, RegEx for Exp)
OptPosInt union of null: Null, value: Int %@@ there must be a better way
OptRegEx union of null: Null, value: RegEx %@@ there must be a better way
StringAIT tuple of
pattern: OptRegEx,
length: OptPosInt,
maxLength: OptPosInt
introduces
string_is_string: List[Char], StringAIT → Bool
asserts
∀
sst: StringAIT
(((tag(sst.length) = null) ∨ (tag(sst.maxLength) = null))
∧ ((tag(sst.length)=value) ⇒ (sst.length.value > 0))
∧ ((tag(sst.maxLength)=value) ⇒ (sst.maxLength.value > 0)))
∀
string: List[Char],
sst: StringAIT
((tag(sst.length) = null
∨ len(string) = sst.length.value)
∧
(tag(sst.maxLength) = null
∨ len(string) <= sst.maxLength.value)
∧
(tag(sst.pattern) = null
∨ string ∈ L(sst.pattern.value)))
[Index]
HTML generated using lsl2html.