ISO/IEC 8613-10:1991

Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications

Traitement de l'information — Bureautique — Architecture des documents de bureau (ODA) et format d'échange — Partie 10: Spécifications formelles

General Information

• Status: Withdrawn
• Publication Date: 03-Jul-1991
• Withdrawal Date: 03-Jul-1991
• ICS: 35.240.20 - IT applications in office work
• Technical Committee: ISO/IEC JTC 1 - Information technology
• Drafting Committee: ISO/IEC JTC 1 - Information technology
• Current Stage: 9599 - Withdrawal of International Standard
• Start Date: 16-Dec-1996
• Completion Date: 12-Feb-2026

Relations

• Amended By: ISO/IEC 8613-10:1991/Amd 5:1993 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 5
• Effective Date: 06-Jun-2022
• Amended By: ISO/IEC 8613-10:1991/Amd 2:1991 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 2: Formal specification of the Raster Graphics content architectures
• Effective Date: 06-Jun-2022
• Amended By: ISO/IEC 8613-10:1991/Amd 4:1992 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 4: Formal specification of the geometric graphics content architectures
• Effective Date: 06-Jun-2022
• Amended By: ISO/IEC 8613-10:1991/Amd 3:1992 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 3: Formal specification of the character content architectures
• Effective Date: 06-Jun-2022
• Amended By: ISO/IEC 8613-10:1991/Amd 1:1991 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 1: Formal specification of the document profile
• Effective Date: 06-Jun-2022
• Revised: ISO/IEC 8613-10:1995 - Information technology — Open Document Architecture (ODA) and Interchange Format — Part 10: Formal specifications
• Effective Date: 15-Apr-2008
• Parent: ISO/IEC 8613-10:1991/Amd 3:1992 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 3: Formal specification of the character content architectures
• Effective Date: 15-Apr-2008
• Parent: ISO/IEC 8613-10:1991/Amd 1:1991 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 1: Formal specification of the document profile
• Effective Date: 15-Apr-2008
• Parent: ISO/IEC 8613-10:1991/Amd 5:1993 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 5
• Effective Date: 15-Apr-2008
• Parent: ISO/IEC 8613-10:1991/Amd 4:1992 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 4: Formal specification of the geometric graphics content architectures
• Effective Date: 15-Apr-2008
• Parent: ISO/IEC 8613-10:1991/Amd 2:1991 - Information processing — Text and office systems — Office Document Architecture (ODA) and interchange format — Part 10: Formal specifications — Amendment 2: Formal specification of the Raster Graphics content architectures
• Effective Date: 15-Apr-2008

Standards Content (Sample)

ISO/IEC
INTER NATIONAL
8613-10
STANDARD
First edition
1991 -06-01
Information processing - Text and office
- Office Document Architecture (ODA)
systems
and interchange format -
Part 10:
Formal specifications
Traitement de l'information - Bureautique - Architecture des documents de
bureau IODA) et format d'échange -
Partie 10: Spécifications formelles
I
I
ISO/IEC 8613-10 : 1991 (E)
Foreword
IS0 (the International Organization for Standardization) and IEC (the International
Electrotechnical Commission) form the specialized system for worldwide standardiz-
ation. National bodies that are members of IS0 or IEC participate in the development
of International Standards through technical committees established by the respective
organization to deal with particular fields of technical activity. IS0 and IEC technical
committees collaborate in fields of mutual interest. Other international organizations,
governmental and non-governmental, in liaison with IS0 and IEC, also take part in the
work.
In the field of information technology, IS0 and IEC have established a joint technical
committee, ISO/IEC JTC 1. Draft International Standards adopted by the joint
technical committee are circulated to national bodies for voting. Publication as an
International Standard requires approval by at least 75 070 of the national bodies
casting a vote.
International Standard ISO/IEC 8613-10 was prepared by Joint Technical Committee
ISO/IEC JTC 1, Information technology.
Development of this International Standard has been in parallel with
- ECMA 101 : 1985, Office document architecture;
- CCITT Recommendation T.37 (1984) : Document interchange protocol for the
telematic services;
- CCITT Recommendations in the T.410 series (1988): Open Document Archi-
tecture (ODA) and interchange format.
IS0 8613 consists of the following parts, under the general title Informationprocessing-
Text and office systems - Office Document Architecture (ODA) and interchange
format :
- Part I: introduction and general principles
- Part 2: Document structures
- Part 4: Document profile
- Part 5: Office document interchange format (ODiF)
- Part 6: Character content architectures
- Part 7: Raster graphics content architectures
- Part 8: Geometric graphics content architectures;
- Part IO: Formal specifications.
NOTE - At present, there are no parts 3 and 9.
Further parts may be added to this International Standard.
Annex A of this part of ISO/IEC 8613 is for information only.
iii
INTERNATIONAL STANDARD ISO/IEC 8613-10 : 1991 (E)
Information processing - Text and office systems - Office
Document Architecture (ODA) and interchange format -
Part 10:
Formal specifications
1 Scope
The purpose of IS0 8613 is to facilitate the interchange of documents.
In the context of IS0 8613, documents are considered to be items such as memoranda, letters, invoices, forms an1
reports, which may include pictures and tabular material. The content elements used within the documents may
include graphic characters, geometric graphics elements and raster graphics elements, all potentially within one
document.
NOTE - IS0 8613 is designed to allow for extensions, including typographical features, colour, spreadsheets and
additional types of content such as sound.
IS0 8613 applies to the interchange of documents by means of data communications or the exchange of storage
media.
It provides for the interchange of documents for either or both of the following purposes:
-
to allow presentation as intended by the originator;
-
to allow processing such as editing and reformatting.
The composition of a document in interchange can take several forms:
- formatted form, allowing presentation of the document;
- processable form, allowing processing of the document;
- formatted processable form, allowing both presentation and processing.
IS0 8613 also provides for the interchange of ODA information structures used for the processing of interchanged
documents.
Furthermore, IS0 8613 allows for the interchange of documents containing one or more different types of content
such as character text, images, graphics and sound.
This part of ISO/IEC 8613
- specifies a formal description technique appropriate for describing the technical specifications of the docu-
ment structures (IS0 8613-2), the document profile (IS0 8613-4) and the content architectures (IS0 8613-6, -7
and -8);
ISO/IEC 8613-10 : 1991 (E)
4 Syntax and semantics of the specification language
This clause describes the formal description technique used for the formal specifications.
NOTE - A tutorial on this formal description technique is given in annex A.
4.1 Basic concepts
IS0 8613 describes document structures, the document profile and the content architectures in terms of abstract
information constructs which are drawn from the following structural categories:
-
An ODA construct may be an atomic construct, e.g. an attribute name or a natural number within an object
identifier.
-
An ODA construct may be a composite construct, i.e. may consist of other constructs. With respect to their
interrelationship, three kinds of composition are distinguished. An ODA construct may be
a) a set;
b) a function (mapping);
c) a sequence (list, string);
of other ODA constructs.
For example, a specific layout description is a set (of constituents), a const#ituent is a nomination (see below) which
is a function or mapping (from attribute names onto attribute values), and an attribute value of ‘subordinates’ or
of ‘object identifier’ is a sequence (of atomic natural numbers).
It is these very structures which are captured by the language used for the formal specifications of IS0 8613. The
language used is called IMCL, Information Modelling by Composiiion Language. The semantics of the specification
language consist of the following abstract elements:
-
the universe which is a non-empty set of entities of the following kinds:
a) constructs;
b) spots;
c) spotsets (i.e. sets of spots);
d) the entity UNDEF (“undefined”);
- functions from the universe to the universe, that is, operators on entities of the universe;
- predicates in the universe, that is, predicates on entities of the universe.
A construct is an information object which is one of the following:
-
an atomic construct or atom, for short;
-
a composite construct or compound, for short, which may be
a) a collection, which is an unordered set of component constructs;
b) a nomination, which is a function that can be regarded as an unordered set of ordered pairs where each
pair consists of a name and a value;
c) a catenation, which is a sequence of component constructs.
The special terminology for composite constructs is to distinguish them from other sets, functions or sequences.
In order to be able to address components in constructs of arbitrary compositional structure, the concept of a
spot is introduced. This concept is an abstract counterpart for the intuitive idea associated with pointing into an
information structure at some position and saying “here”. However, in general the “here” is not identified uniquely
by the component construct as such (e.g. in a word, the same letter may occur several times), but rather by the
context in which it appears. To deal conceptually with the idea of “here” requires a way to identify contexts.
The concept of a spot allows the distinction to be made between a considered construct and its position within a
comprising composite construct of which it is a component. For example, the character string “data” (a catenation)
has the component constructs Id I, ‘a’ and ‘t’. Whereas ‘d’ and It’ appear at one spot each, the la’ appears
at two spots, namely at the second and at the fourth position counted from the front end. So, “data” has four
ISO/IEC 8613-10 * 1991 (E)
logic: not is
NOTE 3: The terminal symbols used in this production rule have the usual semantics of first-order predicai
the logical negation, and. or, (exclusive or), imp1 (implies) and - :fi (if and only if) are the usual logical connectors,
-
V (for all) and 3 (exists) are the logical quantifiers.
prime-formula : : =
[ parameter-part ] predicate-symbol-part .
[ parameter-part predicate-symbol-part .I .[ parameter-part ]
predicate-symbol-part : : =
upper-case-letter [E letter [E digit I. E lower-case-letter [E letter IE digit I. I
= I#II>I~I~l~lClcl>l>
NOTE 4: The semantics of the terminal symbols (=, #, . . . 2) in this production rule are specified in 4.3.
term : :=
var I
constant I
operator-term I
explicit-composition-term I
conditional-term I
extensional-collection-term I
extensional-spotset-term I
spot-selection-term I
( term)
var : :=
lower-case-letter [E letter 1- digit ,. subscript-digit
constant : :=
standard-constant I
nonstandard-constant
standard-constant : : =
UNDEF I
empty-constant I
number-atom-constant
empty-constant : : =
C 1 -. empty collection .- I
C : 3 -. empty nomination .- 1
C -+ 1 -. empty catenation .- I
< > -. empty spotset .-
number-atom-constant : : =
- E] digit [E digit I. [E . E digit [E digit I.]
[+
nonstandard-constant : : =
I E character [- character I. E I -. restriction on apostrophe occurrence .-
operator-term : : =
[ parameter-part ] operator-symbol-part , .
[ parameter-part operator-symbol-part .I .[ parameter-part 3
operator-symbol-part : : =
upper-case-letter [G upper-case-letter IZ digit IE - I. I
"I+l-l*lllul"l\lNI I'lllt
NOTE 5: The semantics of the terminal symbols (-, +, . . . T) in this production rule are specified in 4.4.
explicit-composition-term : : =
Cterm [ ; term J. I -. collection .- 1
[term : term [ ; term : term I. 3 -. nomination .- I
C -+ term [- term] . -+] -. catenation .- I
" E character [- character I. G " -. catenation of characters, restriction on quote occurrence .-
ISO/IEC 8613-10 : 1991 (E)
4.3 Predicate symbols with built-in semantics
A sequence of predicate-symbol-parts is referred to as a predicate symbol. For each n-ary predicate symbol there
is an n-ary predicate on the universe of the specification language, i.e. an n-ary relation on entities of the universe.
Some predicate symbols have built-in semantics which are introduced by the following.
NOTE - The predicate-symbol-parts are syntactically distinguished from operator-symbol-parts and variables.
True means the valid fact (something stated as being true)
False means the invalid fact (something stated as being false)
IsAtom(t) means t is an atomic construct or atom, for short
IsNat(t) means t is a natural number (1, 2, . . . ; zero excluded)
IsInt (t) means t is an integer number (. . . -2, -1, O, 1, 2, . . .)
IsReal(t) means t is a real number
IsCol(t) means t is a collection
IsNom(t ) means t is a nomination
IsCat (t) means t is a catenation
Isspotset (t) means t is a spotset
IsSingle (t) means t is a singleton spotset
tl =t2 means tl is equal to t2 (all entities)
means - not tl = t2
tl # t2
means tl is less than t2 (numbers)
tl < t2
means tl is less than or equal to t2
tl 5 t2
means tl is greater than t2
tl > t2
means ti is greater than or equal to t2
tl L t2
means ti is element of t2 (collections)
tl E t2
means - not tl E t2
tl 6 t2
tl € t2 means tl is singleton spotset and subset of t2 (spotsets)
means tl is subset of t2 (collections or spotsets)
tl c t2
means tl is subset of or equal to 12 (collections or spotsets)
11 c_ 22
means
t2 is subset of tl (collections or spotsets)
tl 2 t2
means t2 is subset of or equal to tl (collections or spotsets)
tl 2 t2
The unary predicate symbols mean predicates for expressing that an entity belongs to a certain class or “type” of
entities, i.e. has a particular property. The binary predicate symbols refer to predicates which indicate whether or
not a particular relationship holds for two entities.
4.4 Operator symbols with built-in semantics
A sequence of operator-symbol-parts is referred to as an operator symbol. For each n-ary operator symbol there
is an n-ary operator or function from the universe to the universe of the specification language, i.e., a mapping
from n-ary tuples of entities onto entities of the universe. Some operator symbols have built-in semantics which are
introduced by the following.
NOTE - The operator-symbol-parts are Syntactically distinguished from predicate-symbol-parts and variables. For all
operators it holds that the result is UNDEF, if a parameter term does not meet the requirement stated below.
Ct If t denotes a singleton spotset, C t denotes the component construct at the spot
given by t.
Nt If t denotes a singleton spotset of a spot that is a component of a nomination
(“immediately inward” of a nomination is the formal term), then N t denotes
the name construct of the component as it is within the nomination.
Ft If t denotes a set of exactly one spot immediately inward of a catenation spot,
F t denotes the front part of this catenation up to but excluding the component
given by t (catenation of components with lower position than t).
ISO/IEC 8613-10 : 1991 (E)
If mi denote constructs, the whole term denotes the catenation which contains
the constructs mi as components - also referred to as members - in the indi-
cated sequence. (This is an example for explicit-composition-term)
Denotes the catenation [ -+ 'O' -+ 'DI --+ 'A' -+ ' ' +. 'P' -+ lai --+ Ir' -+
"ODA Part 2'
It' -+ I ' --+ '2' -+ 3. A string of characters enclosed in quotes denotes the
catenation of those characters. A pair of quotes in the string stands for a single
one in the catenation. (This is an example for explicit-composition-term)
Denotes the empty catenation. (This is an example for empty-constant)
[--+I
<> Denotes the empty spotset. (This is an example for empty-constant)
IF formula THEN tl ELSE t2 If tl and t2 are terms, the whole term denotes the same as tl or ta, depending
on whether the formula is True or False, respectively. (This is an example for
conditional-term)
C war I formula1 Denotes the collection of all constructs war which satisfy the formula. (This is
an example for extensional-collection-term)
< wa.r I formula > Denotes the spotset which is the union of all singleton spotsets war which satisfy
the formula. (This is an example for extensional-spotset-term)
t If t denotes a (possibly empty) spotset, the whole term denotes the union of
all singleton spotsets war which contain a spot taken from t and for which the
formula is True. (This is an example for spot-selection-term)
Three elliptic notations are provided for frequently occurring spot-selection-
clauses:
t < formula > If a variable var is not introduced explicitly, the abbreviated term
t < formula > is evaluated for the standard variable zs (singleton set of the spot
under examination or examination spot, for short). (This is an example for
spot-selection-term)
If the formula has the structure
N war = n1 E N war = 722 0: .
where ni are name-specifications, the formula may be abbreviated as a list of
name-specifications. (This is an example for spot-selection-term)
If there is only one name-specification n used for spot selection, an elliptic-
spot-selection-term is provided as an abbreviation of special spot-selection-terms
(ending with , etc.). The n stands for (see name qualification in
programming languages). (This is an example for elliptic-spot-selection-term)
-
4.6 Notational simplifications
The common notational simplifications for successive logical quantifications can be used. The following examples
explain these "short-hand" notations which are usually applied in first-order predicate logic:
The expression V z(V y(3 z(formu1a)))
may be written as V zV y3 z (formula)
or even as Vz,y 32 (formula)
A further abbreviation is used to help emphasize the "essential part" of a quantified formula:
The expression Vz(z E m impi formula )
-
may be written as
Vz E m (formula )
and 3 z(z E m and formula )
may be written as
3 2 E m (formula )
This notation can be combined with the previous one:
The expression Vz(z E m imp1 Vy(3z(z E p formula)))
-
ISO/IEC 8613-10 : 1991 (E)
Structure of the formal speciflcations
This clause outlines the general concepts for the formal specifications. Those terms which are used at several places
throughout the formal specifications are contained in clause 6.
Formally speaking, each of these formal specifications is a single formula in first-order predicate logic. This formula,
being given near the beginning of each formal specification, is called the overall formula. The formula consists of
other formulae which are connected by and:
formulai and formula2 & formula3 . formula,
In the present context, each of these formulae is called a “definition” and identified through a unique reference
number. A definition defines either a concept used in the narrative part of IS0 8613 or a concept which has a
subsidiary function in the network of definitions in that it has been separated and “encapsulated” to render other
definitions more readable.
The definitions are grouped into several subclauses. For example, within the formal specifications of the document
structures the definitions relating to the sets of constituents are contained in 7.1, those relating to constituents
in 7.2 and those relating to attributes in 7.3. In addition, concepts which are not used in the formal specification
but are used in the text of the IS0 8613-2 are defined in 7.5.
The “factorization” of definitions is only for the convenience of authors and readers; it does not in any way impair
the formal rigidity of the approach.
Variables occurring in the definitions are always bound by universal (V) or existential (3 ) quantifiers. Therefore,
once a value has been chosen for a variable it has to be retained throughout the scope of the quantifier wherever
the variable appears.
All predicates apart from those pertaining to the specification language are defined using the same format. For
unary predicates the format is:
V variable (predicate-symbol(variab1e) - zfl formula)
A similar format is applied for n-ary predicates. There, the variables have been placed around the predicate symbol
in a “natural” way, e.g. (id)IsIdContIn(b) is expected to be read as “id is an identifier of a content portion in the
basic object b”.
A “predicate” in first-order predicate logic is a propositional pattern where some places are left free for the insertion
of individual entities. An example is the pattern “. . .is greater than . . . ”. Once the free places have been occupied
by entit8ies, the pattern becomes a proposition for which the ‘‘t,ruth value” can be evaluated. The proposition “5 is
greater than 2” evaluates to True, whereas the propositions “3 is greater than 5” and “a Mercedes is greater than
SC 18” evaluate to False. Note that a proposition may never evaluate to an undefined truth value.
A unary predicate is a pattern with only one free parameter place, Its definition is evaluated by substituting an
individual entity for the parameter. This yields a proposition on the left-hand side of the - aff and transforms the
whole expression in parentheses into a proposition.
A uniform format has also been adopted for the definition of most operators. It relies on the conditional-term of
the specification language:
Vvariable (operator-symbol(wariab1e) = IF formula THEN term ELSE UNDEF)
An “operator” is a term pattern where some places are left free for the insertion of individual entities. An example
is the pattern “. . .plus . . .”. Once the free places have been occupied by entities, the pattern becomes a term,
i.e. an expression which evaluates to or denotes an individual entity. The term “5 plus 2” denotes the entity 7,
whereas the term “WG 3 plus SC 18” denotes the entity which is represented by UNDEF in the formal specification
language. Therefore, a term evaluates to “undefined”, if the operator is not defined for the inserted entities.
It should be noted that the formal specifications cannot be applied directly to the Office Document Interchange
Format (IS0 8613-5) and the reader should not necessarily expect to see any direct correspondences. The formal
specifications are based on the textual description of the concepts of IS0 8613 and do not necessarily reflect the
ODIF encoding of ODA documents. Those clauses in IS0 8613 which specify the ODIF encoding usually impose
additional rules for the make-up of the interchanged data stream. These additional rules are considered outside
of the scope of the formal specifications: The ODIF encoding specifies these additional rules formally and there is
therefore no need for repeating these additional riiles in FODA.
ISO/IEC 8613-10 : 1991 (E)
6 Commonly used definitions
This clause contains those definitions which are not specific to the formal specification of the document structures,
the document profile or one of the content architectures only.
I semiformal Descrithon 1.1 I
Predicate “is a non-empty collection”
An entity col is a non-empty collection (set of constructs) if it is a collection which is not empty.
I Definition 1.1 ]
1 Vcol
2 (,IsNeCol(col) zfl
IsCol(c0l) dol # c 1 ,)
I Semiformal Descrbtion 1.2 1
I I
Predicate “is a non-empty nomination”
An entity nom is a non-empty nomination (mapping of names onto constructs) if it is a nomination which is not
empty.
I Definition 1.2 I
1 Vnom
2 (,IsNeNom(nonz) if
3 IsNom(nom) Jnom # C : 1 ,)
1 semiformal Descri~tiori 1.3 I
i I
Predicate “is a non-empty catenation”
An entity cat is a non-empty catenation (sequence of constructs) if it is a catenation which is not empty.
I Definition 1.3 I
1 Vcat
2 (,IsNeCat(cat) ifl
IsCat(cat) &cat # c + I ,,)
I Semiformal Description 1.4 I
Predicate “is an empty collection”
An entity col is an empty collection if it contains no components.
I Definition 1.4 I
1 Vcol
2 (,, IsEmptyCol(col) - iff
3 col = c 1,)
ISO/IEC 8613-10 : 1991 (E)
c
I Semiformal Description 1.9 I
Predicate “is a pair of positive integers”
A pair of positive integers is a catenation of two positive integers.
I Definition 1.9 I
1 Vq
2 (,IsPairOfPosInt(q) - zfl
3 31,r
(,q = C -+ 1 + r + 1 and IsNat(1) & IsNat(r),),)
I Semiformal Description 1.10 I
Predicate “is an octet string”
An octet string is an atomic construct in the formal specification.
I Definition 1.10 I
a 1 vu
2 (, IsOctetString(v) - zfl
3 IsAtom(v),)
1 Semiformal Description 1.11 I
Function “position from the front end”
PF returns the position number of the indicated component, the count beginning with the first component and
ending at and including the considered component. The operand p is required to denote a set of exactly one spot
immediately inward of a catenation.
I Definition 1.11 I
1 VP
2 (OWPI =
3 IF IsSingle(p) and IsCat(C p’)
THEN LENGTH’.l‘ (F p) + 1
5 ELSE UNDEF,)
a
I Semiformal Description 1.12 I
Function “position from the rear end”
PR returns the position number of the indicated component, the count beginning with the last component and
ending at and including the considered component. The operand p is required to denote a set of exactly one spot
immediately inward of a catenation.
I Definition 1.12 1
1 VP
2 (,PR(P) =
3 IF IsSingle(p) IsCat(C p’)
4 THEN LENGTH1.lG (R p) + 1
5 ELSE UNDEF,)
ISO/IEC 8613-10 : 1991 (E)
I Semiformal Description 1.17 1
Function “collection of component constructs”
COLC returns the collection of the component constructs at the spots of the (possibly empty) spotset ss.
I Definition 1.17 J
1 vss
2 (,COLC (ss) =
3 IF IsSpotset(ss)
4 THEN Cg13pÊss(g=Cp)l
5 ELSE UNDEF,)
I Semiformal DescriDtion 1.18 1
Function “name set of a nomination”
NAMS returns the name set of the given nomination n, i.e. the collection a. names c
the components c the
nomination.
1 Definition 1.18 I
1 VIZ
2 (,NAMS(n) =
3 IF IsNom(n)
4 THEN Cm13pÊ -ni (m= N p)l
5 ELSE UNDEF,)
I Semiformal Description 1.19 I
Predicate “is the placeholder for any attribute value”
An entity U is the placeholder for the value of a defaultable attribute if it is the atom with this particular interpre-
tation.
NOTE - The term ‘placeholder for any attribute value’ is not an IS0 8613 attribute value but a construct which is
introduced to achieve consistency throughout the formal specifications and to distinguish between mandatory and defaultable
or parameters. The actual value is dependent on the respective attribute and the defaulting rules and will be
attributes
determined during the processing of a document (editing process, layout process, imaging process) whenever a value for a
defaultable attribute or parameter is needed.
I Definition 1.19 1
1 vu
2 IsPlaceholder(u) - ifl
3 U = I placeholder for any attribute value’ ,)
I Semiformal DescriDtion 1.20 1
Predica.te ‘‘is an IS0 6937 minimal subrepertoire string”
An IS0 6937 minimal subrepertoire string is a catenation of IS0 6937 minimal subrepertoire characters.
1 Definition 1.20 I
1 vu
2 IsIS06937MSString(u) zfl
3 I~NeCatl.~(u) and V rn î-u (I~IS06937MSCharacter’.~~(C m)),)
ISO/IEC 8613-10 : 1991 (E)
I Semiformal Description 1.25 1
Predicate “is a positive real number”
A positive real number is a real number whose value is greater than zero.
I Definition 1.25 1
1 vv
2 (,IsPosReal(v) ifl
3 IsReal(v) &v> 0.0,)
ISOIIEC 8613-10 : 1991 (E)
- and . . . IsBasicLayout Ob jectClassDescription2 35 (cst ) . . .
- and . . IsBasicObject ClassDescription2 36( cst) ., ,
- and . IsObjectClassDescription2 37(~st) .
- and . IsRootDescription2 38(cst) .
- and . . IsLogicalRoot Description2 39( cst) . .
- and . . IsCompositeLogica10bjectDescription2 40( cst) . .
- and . . IsBasicLogicalOb jectDescription2 41 (cst) . .
- and . . IsLogica10bjectDescription2 42 (cst) .
- and . . IsLayoutRootDescrip tion2 43( cst) .
- and . IsPageSetDescription2 44(~st) .
- and . . IsCompositePageDescription2 45(~st) . .
- and . IsBasicPageDescription2 46(~st) .
- and . IsPageDescription2 47(~st) .
- und . IsFrameDescription2 48(cst) .
- and . IsBlockDescription2 49(~st) .
- and . IçLayoutObjectDescription2 50(~st) .
- and . . IsCompositeObject Description2 51 (cst) . .
- and . . IsBasicObject Description2 52( cst) . .
& . IsCompositeLayoutObjectDescription2 53(~st) .
- and . . IsBasicLayoutObjectDescription2 54 (cst) . .
- and . IsObjectDescription2 55(~st) .
- and . . . Iscontent PortionDescription2 56 (cst ) . . .
- and . . IsCharacterContentPortionDescription2 57( cst) . .
- and . IsRasterGraphicsContentPortionDescription2 58(cst) .
- and . IsGeometricGraphicsContentPortionDescription2 59(~st) .
- and . IsLayoutStyle2 60(cst) .,
- and . IsPresentationStyle2 61 (cst) .
-.attributes: .-
- and . IsAttributeSet2 62(m) .
- and , . IsProfileAt trib~teSetPart2~ 63(as) . . .
- and . IsBindingsValueExpression2 64(v) , .
- and . IsStringExpression2 65(v) .
- and . IsAtomicStringExpression2 "(U) .
- and . IsStringFunction2 67(~) ,.
- and . IsNumericExpression2 "(v) .
- and . IsNumericFunction2 "(U) .
and . IsObjectOrObjectClassIdExpression2 "(U) .
g& . . IsObjectOrObjectClassSelectionFunction2 7f (v) . .
- and . IsBindingReferenceExpression2 72(v) .
- and . IsBindingReference2 73(v) .
- and . IsBindingName2 "(v) .
- and . IsBindingSelectionFunction2 "(U) .
- und . . . IsCurrentInstanceFunction' 76 ( v) . . .
... IsObjectTypeValue2 77(v) ...
- and . IsLogica10bjectId2 7"(v) .
- and . IsLayoutObjectId2 7g(v) .
- and . IsObjectId2 "(v) .
- and . IsLogica10bjectClassId2 "(U) .
- and . . IsLayout Object ClassId2 82( v) . .
- and . IsObjectClassId2 "(v) .
- and . IsSeqOfObjectClassId2 "(U) .
g& . IsConstructionExpression2 "(v) .
and . IsConstructionType286(v) .
ISO/IEC 8613-10 : 1991 (E)
- und . . (sl~g)IsContainedIn~.~~~ (slay) . .
- und . . (id)IsClassIdImSubIn2~142 (gco) . .
- und . . (id)I~IdImSubIn~.~~~( sco) . .
- und . . (id)I~IdContIn~.~~~ (b) . .
- und . . (idq)IsSeqClas~IdImSubIn~.~~~ (gco) . .
- und . . (idq)C~veredBy'.l~~( T-) . .
- und . . (id)O~cursIn~.'~~(rn) .
- und . . (go)IsInitialGeneri~In~.~~"(gos) . .
- und . . (so)IsInit ialSpecifi~In~.~~~( SOS) . .
- und . (Igo)Des~ribesClassIrnSubOf~~~~~(hgo) .
- und . (Igo)Des~ribesClassSubOf~~~~~(hgo)In(g) .
- und . . (iso)Des~ribesIrnSubOf~~~~~( hso) . .
- und . . , (cont)Describe~ContPortOf~.~~~( b)
NOTE - Other predicates or operators which are used here, but are defined in clause 6, are not listed here.
In principle a given interchange set may be verified to conform to IS0 8613 by establishing
AS - imp1 IsInterchangeSet2.1(-.this-terrn.-)
where AS stands for the conjugation of all axioms and definitions and the argument of IsInterchangeSet stands
for a formal expression (a term) which denotes the particular interchange set in question. If the extended overall
formula yields True, the document description conforms to IS0 8613, if False, it does not. An undefined result is
impossible.
ISO/IEC 8613-10 : 1991 (E)
I Semiformal Description 2.3 I
Predicate "is a document description" (2.3)
An entity doc is a document description if it is a document profile prof (5) or if it is an entity which is pro-
cessable, formatted processable or formatted (5-6), according to the value of the document profile attribute
'document architecture class' (7-13)' with a 'resource document' specified in the profile if any 'resource' is specified
in the document (14-15).
I Definition 2.3 I
1 V doc
2 IsDocumentDescription(doc) - iff
3 prof
4 (1 IsDocumentProfilePart22~20(prof) and
5 (2 doc = [pro fl 0: IsPr~cessable~~~(doc) E
6 IsFormattedProcessable2~5(doc) E IsFormatted2.6(doc) J &
7 doc # [prof] impl
-
8 (3(4C -prof. 'document architecture class' = 'processable' iff
-
9 IsPro~essable~.~ (doc) *) & .
10 (5 C -prof 'document architecture class' = 'formatted processable' zff
-
11 IsFormattedProcessable' 5(d~~),) &
C ^prof ' document architecture class' = 'formatted
iff
-
13 IsFormatted2,6(doc),) &
14 V cst E doc
15 (, 'resource' E NAMS1.la(cst) - impl 'resource document ' E NAMS1.18(prof) ,)3)l)o)
ISO/IEC 8613-10 : 1991 (E)
I semiformal DescriDtion 2.5 I
Predicate "is formatted processable" (2.3.6, 2.3.11, 8.2)
An entity doc is formatted processable if it is a collection of constituents consisting of a document profile prof along
with a document body doby (4,5) which includes (possibly empty) constituent sets glog, slog, glay, slay, laystys
and prestys (6). Attributes in the document profile indicate the presence of a specific logical description, the
specific layout description, the generic layout description (these three sets are always present) and of (optionally)
a generic logical description, layout style set and presentation style set (7-15). If the value of the profile attribute
'generic logical structure' is 'complete generator set I, the specific logical description slog is completely described
by the generic logical description glog (16,17). If the value of the profile attribute 'generic layout structure' is
'complete generator set', the specific layout description slay is completely described by the generic layout description
glay (18,19). The specific logical description is contained in the specific layout description (20). The profile attribute
'document architecture class' has the value 'formatted processable' (21). The document profile and the document
body satisfy the constraints imposed by the content architectures (22-24).
I Definition 2.5 I
1 V doc
2 IsFormattedProcessable(doc) 2ff
3 3prof,doby, glog, slog, glay, slay, laystys,prestys
4 doc = [prof] ü doby
5 IsDocumentProfilePart22 20(prof) and IsDocumentBody2 7(doby) and
6 doby = glog U slog U glay U slay ü laystys U prestys and
7 'specific logical structure' E NAMS' '"(prof) & IsSpecificLogicalDescription' 13(s10g) and
8 'specific layout structure E NAMS' "(prof) & IsSpecificLayoutDescription' 14(slay)
9 'generic layout structure' E NAMS' "(prof) & IsGenericLayoutDescription2 ll(glay) &
(2 'generic iogicai structure' E NAM^ '"(prof) 28
11 (3 IsNeCol' '(glog) IsGenericLogicalDescrKtion' 'o(glog),),)
12 (4 I layout styles' E NAMS~ '"(prof) 28
(5 IsNeCol' '(laystys) and IsLayouZtyleSet' 15(laystys),),) and
(6 'presentation styles' E NAMS~ '"(prof) 28
15 (, IsNeCol' (prestys) and IsPresentatioZtyleSet' 16(prestys) 7)6) &
16 (8C -prof 'generic logical structure' = 'complete generator set' zmpi
-
17 (sZog)IsCompletelyDescribedBy2 136(g10g) ,) and
18 (9C -prof. 'generic layout structure' = 'complete generator set' zmpl
-
19 ( sZay)IsCompletelyDescribedBy2 136 (gla y) ,) and
20 (sZog)IsContainedIn2 14' (slay) and
21 C "prof. 'document architecture class' = 'formatted processable' &
22 SatisfiesCharacterContentArchitectureConstraints' 17(prof, doby) &
23 SatisfiesRasterGraphicsContentArchitectureConstraints2 '"(prof, doby) and
24 SatisfiesGeometricGraphicsContentArchitectureConstraints' lg(prof, doby) JO)
ISO/IEC 8613-10 : 1991 (E)
I Definition 2.7 I
1 V doby
2 (, IsDocumentBody(doby) - ifl
3 3 glog, slog, glay, slay, laystys, prestys
4 (, doby = glog U slog U glay ü slay U laystys U prestys &
5 (, IsNeCol'.' (glog) - impl IsGenericLogicalDescription2.10 (glog ) ,) &
6 (,IsNeCol'.'(slog) - impl IsSpecificLogicalDescription'~'3(slog)3) and
(,IsNeCol'.'(slay) - impl IsSpecificLayoutDescription2~'4(slay),) &
8 (,IsNeCol'.' (glay) - impl IsGenericLayoutDescription'.'' (glay),) &
9 (,IsNeCol'.'(laystys) - impl IsLayoutStyleSet2~15(laystys),) and
10 (, IsNeCol'.' (pest ys) - impl IsPresentationStyleSet','6 (prestys) ,) &
(, (, IsNeCol'.'(slog) & IsNeCol'.'(glog),) - impl (sl~g)IsDescribedBy~.'~~(glog),) and
12 (lo (,, IsNeCol'.'(slay) and IsNeCol'~f(glay),,) - impl (slay)I~DescribedBy~~~~~(glay),,) and
13 Vest E (glog ü slog) (,,Vx E ^at. (N 2 = 'layout style') - impl
14 (13 3 Is E laystys (C -1s. layout style identifier ' = C z)
,,) and
15 Vcst E (glog U slog ü glay U slay) (14Vz E ^cst. (N z = ' presentation style') - impl
16 (is3ps E prestys (C ^ps. 'presentation style identifier' = C x)
&
17 Vcst E laystys (16Vy G ^at.
18 (1, (,,1s0bjectC1ass1d2~"3(C y) - imp1
19 (,,3go E glay (C ^go. 'object class identifier' = C y) ,,),,) &
20 (,, IsLayoutCatN âme2.' '' (C y) imp 1
-
21 (,, 3 is E laystys (C -1s. I layout category' = C y) ,,),,) &
22 V1,r
(,, (,, (,4 N y = 'same layout object' C y = C + 1 + r + 1 and IsObjectClassId2~"(r) ,,) impI
24 (,,3go E glay (C ^go. 'object class identifier' = r) ,,),,) &
25 (,,(,,N y = 'same layout object' & C y = C + I -+ r + 1 & IsLayoutCatName2.1'2(r) ,,)
26 (,,3Is E laystys (C -1s. 'layout category' = r) ,,),,),,),,),,) and
27 Va ^glay. . 'logical source'
28 (,, 3go E glog (C ^go. ' object class identifier ' = C a) ,,) &
29 Va e ^slay. . 'balance'
30 (30C a # 'nuII' impl
-
31 Vb G ^(C a). (313so E slay (C ^SO. 'object identifier' = b)31)30) &
Va e ^glay . . ' balance '
33 (3, C a # null impl
-
34 V b G ^(C a). (333go E gIay (C ^go. 'object class identifier' = b)33)3z) and
35 Vcst E slay
36 (34 (C'imaging order'; 'subordinates1] c NAMS'.'"(cst)) - impl
37 Cz I z 6 ^est. 'imaging order'] = Cy I y i? ^est. 'subordinates'l,,),),)
ISO/IEC 8613-10 : 1991 (E)
Predicate “is a generic logical description” (2.3.12, 3.5.6)
An entity glog is a generic logical description if it is a generic description containing only logical object class
descriptions and content portion descriptions (46). For a content portion description the attribute content identifier
logical ’ is present and its value is a generic logical identifier.
I Definition 2.10 1
V dog
IsGenericLogicalDescription(glog) - zfl
IsGenericDescription2.”(glog)
Vcst E glog
(1 IsLogica10bjectClassDescription2.25(cst) oy
IsContentPortionDescription2~56 (cst) and
‘content identifier logical I E NAMS’.”(cst) and
IsLogica10bjectClassId2.al(C ^est. ‘content identifier logical
l)o)
I Semiformal Description 2.11 I
Predicate “is a generic layout description” (2.3.12)
An entity giay is a generic layout description if it is a generic description containing only layout object class
descriptions and content portion descriptions (4-6). For a content portion description the attribute I content identifier
layout’ is present and its value is a generic layout identifier.
I Definition 2.11 I
Vday
IsGenericLayoutDescription(glay) zff
IsGenericDescription2.”(glay) and -
V cst E giay
(1 IsLayoutObjectClassDescription2.32 (cst)
(2 IsContentPortionDescription2~56(cst) and
I content identifier layout I E NAMSl.’’(cst) and
IsLayoutObjectClassId2.”2(C ^est. ‘content identifier layout 1)2)1)o)
ISO/IEC 8613-10 : 1991 (E)
1 Semiformal Description 2.14 I
Predicate "is a specific layout description'' (2.3.12, 3.3.1, 5.4.2.1)
An entity slay is a specific layout description if it is a specific description containing only layout object descriptions
and content portion descriptions (46). For a content portion description the attribute I content identifier layout
is present and its value is a specific layout identifier (7-8). The immediate subordinates of the layout root or a
page set are page sets and/or pages (9-11). The immediate subordinates of a composite page are frames and/or
blocks (12-15). The immediate subordinates of a frame are frames and/or blocks (16-19). If blocks are immediate
subordinates of a constituent, the attribute balance' must not be specified for this constituent (15, 19), otherwise
it must be present or it is defaulted.
I Definition 2.14 I
1 V slay
2 (,, IsSpecificLayoutDescription(s1ay) ifl
3 IsSpecificDescription2.12 (slay) &-
4 Vest E slay
5 (2 IsLayout Ob jectDescripti~n~.~~ (cst ) E
6 (3 IsC~ntentPortionDescription~.~~(cst) and
7 'content identifier layout I E NAMSl.'"(cst) and
8 IsLay~utObjectId~.~~(C *est. 'content identifier layout') 3)2) &
9 (4 (5 IsLayoutRootDescription2~43( cst) IsPageSetDe~cription~.~~( cst) J - impl
10 Vso E IMSUB2.154(~st, slay)
11 (IsPageSetDe~cription~.~~(so) E IsPageDe~cription~.~~(so)) 4)
12 IsComp~sitePageDescription~.~~(c~t) - impl
Vso E IMSUB2.154(~st,slay)
(, (IsFrarneDe~cription~~~"(so) & balance' E NAMS'.'"(cst)) E
(IsBlockDescription2~49(so) & ' balance' 6 NAMS'.'"(cst)) ,),) g&
(e IsFr ameDescr ip ti~n~.~" (cst ) - imp 1
17 Vso E IMSUB2.154(~st,slay)
18 (9 (IsFrameDescription2~4"(so) & I balance E NAMS'.'"(cst))
19 (IsBlockDescription2.49(so) and I balance' 6 NAMS'.'"(cst)) ,),),),)
I Semiformal Description 2.15 I
Predicate "is a layout style set" (2.3.5)
An entity laystys is a layout style set if it is a non-empty collection of layout styles (3,4) whose identifiers are unique
within that collection (5-7).
I Definition 2.15 I
1 Vlaystys
2 (, IsLayoutStyleSet(laystys) - Zfl
3 IsNeCol'.'(laystys) g&
4 ~cst E laystys (IsLayoutStyle2.60(cst))
5 V x, y E laystys
6 (lx #Y - imp!
7 C -x 'layout style identifier' # C -y. 'layout style identifier' ,),)
ISO/IEC 8613-10 : 1991 (E)
7.2 Constituents
In constituents, the values of defaultable attributes need not be specified explicitly - as opposed to mandatory
or non-mandatory attributes. In these cases the formal specification provides a placeholder for the value which is
either specified elsewhere in the document description or specified in the International Standard as the default value
(5.1.2.4). Such a "dummy value" is formally defined as satisfying the predicate IsPla~eholder~.~~.
I Semiformal DescriDtion 2.20 I
Predicate '5s a document profile of Part 2" (IS0 8613-4, 5.2)
(The formal specification of the document profile has only been carried out here, as far as it is necessary for the
formal specification of the document structures described in IS0 8613-2.)
A document profile is a set of profile attributes (as far as required for IS0 8613-2). The attribute I document architec-
ture class' is a mandatory attribute (4) and its value is either 'formatted I, 'processable' or 'formatted processable'.
If the value of the attribute 'document architecture class' is ' processable', and the attributes 'generic layout
structure' and 'specific logical structure', but not 'specific layout structurel are specified, the value of the attribute
'generic layout structure' is 'complete generator set' (6-10). If the valueof the attribute 'document architecture class'
is 'formatted processable', and the attributes 'generic layout structure', 'specific logical structure' and 'specific lay-
out structure' are specified, the value ofthe attribute 'generic layout structure' is 'complete generator set' (11-15). If
the value of the attribute 'document architecture class' is 'formatted I, and the attributes 'generic layout structure'
and 'specific layout structurel but not 'specific logical structure' and 'generic logical structure' are specified, the
value of the attribute 'generic layout structure' is either I partial generator set' or 'factor set I (16-21).
[ Definition 2.20
v prof
2 IsDocumentProfilePart2(prof) - zff
3 IsProfileAttrib~teSetPart2~ 63(prof)
4 'document architecture class' E NAMS' "(prof) and
5 C -prof. 'document architecture class' E ['formatted I; ' processable'; 'formatted processable'] &
6 (1 (,C -prof. 'document architecture class' = ' processable' &
7 'specific iogicai structure' E NAMS' "(prof)
8 'specific layout structure I 6 NAMS' "(prof) &
9 (3 'generic layout structure' E NAMS~ 18(prof) imp1
-
10 C -prof. 'generic layout structure' = 'complete generator set' J2) E
11 (4 C 'prof. 'document architecture class' = 'formatted processable' and
12 'specific iogicai structure' E NAMS' "(prof) and
13 'specific layout structure' E NAMS~ "(prof) and
14 'generic layout structure' E NAMS' "(prof) and
15 C -prof. 'generic layout structurel = complete generator set ,) oy
16 (,C -prof. 'document architecture class' = 'formatted' &
17 'specific iogicai structure' 6 NAMS' "(prof) and
'generic iogicai structure' 6 NAMS~ "(prof) and
19 'specific layout structure' E NAMS~ "(prof) and
20 (6 'generic layout structure' E NAMS' 18(prof) e
21 C -prof. 'generic layout structure' E C'partial generator set';'factor set'] 6)6)1)o)
ISO/IEC 8613-10 : 1991 (E)
I Semiformal Description 2.23 I
Predicate "is a composite logical object class description" (3.5.6)
A composite logical object class description is a logical root class description or an attribute set (nomination) which
may contain the attributes 'application comments', bindings', 'default value lists', 'generator for subordinates',
' layout style', 'object class identifier I, ' object type', ' protection I, I resource , I user-readable comments' and ' user-
visible name'. The attributes 'object class identifier' and 'object type' are both required and have a logical object
class identifier and a 'composite logical object' as respective values (14-15). None of the attribute values is default-
able (13).
I Definition 2.23 I
1 v cst
2 (,IsCompositeLogicalObjectClassDescription(cst) _. ifl
3 IsLogicalRootClassDescription2.22(cst)
4 IsAttributeSet2 62(~st) &
5 NAMS'.''(CS~) >. ['object class identifier'; 'object type'] und
6 NAMS'.''(CS~) C ['application comments'; ' bindings';
7 'default value lists'; 'generator for subordinates';
8 ' layout style' ; 'object class identifier ';
9 object type ' ; protection
...