XML Schema Documentation
Schema Document Properties
| Target Namespace | https://www.atelierb.eu/Formats/pog |
|---|---|
| Element and Attribute Namespaces |
|
The purpose of this document is to describe and illustrate
the POG format: an XML representation of the proof obligations
for a B component or for an Event-B component.
* This documentation corresponds to version 1.0 of the format.
* The root element is always a
[Proof_Obligations](#element_Proof_Obligations "Definition of element Proof_Obligations").
Proof obligations are essentially combinations of B
predicates. An important part of the format describes how B
predicates, expressions and types are represented. This
description references the B Language Reference Manual, version
1.8.10 as *BLRM*.
### Licensing
© 2019 by CLEARSY Systems Engineering.
This work is available under a [Creative Commons
Attribution-NonCommercial 4.0 International (CC-BY-NC)
License](http://creativecommons.org/licenses/by-nc/4.0/).
| Prefix | Namespace |
|---|---|
| Default namespace | https://www.atelierb.eu/Formats/pog |
| xml | http://www.w3.org/XML/1998/namespace |
| xs | http://www.w3.org/2001/XMLSchema |
Global Declarations
Element: Binary_Exp
Represents a binary expression.
* Two child elements represent the arguments.
* Attribute `op` represents the operator and shall be a
[binary_exp_op](#type_binary_exp_op).
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Binary_Exp op="binary_exp_op" [1] typref="xs:integer" [1] tag="xs:string" [0..1] > Start Group: exp_group [2..2] Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice End Group: exp_group </Binary_Exp>
<xs:element name="Binary_Exp"> <xs:complexType> <xs:group ref="exp_group" minOccurs="2" maxOccurs="2"/> <xs:attribute name="op" type="binary_exp_op" use="required"/> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Binary_Pred
Represents a binary predicate.
* Two child elements represent the arguments.
* Attribute op represents the operator and shall be a
[binary_pred_op](#type_binary_pred_op).
<Binary_Pred op="binary_pred_op" [1] > Start Group: pred_group [2..2] Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice End Group: pred_group </Binary_Pred>
<xs:element name="Binary_Pred"> <xs:complexType> <xs:group ref="pred_group" minOccurs="2" maxOccurs="2"/> <xs:attribute name="op" type="binary_pred_op" use="required"/> </xs:complexType> </xs:element>
Element: Boolean_Exp
Representation the conversion of a predicate to a Boolean
expression.
* A single child element represents the converted predicate.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Boolean_Exp typref="xs:integer" [1] tag="xs:string" [0..1] > Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice </Boolean_Exp>
Element: Boolean_Literal
Represents a Boolean literal expression.
* Attribute `value` is the represented literal and is of
type [boolean_literal_type](#type_boolean_literal_type).
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Boolean_Literal value="boolean_literal_type" [1] typref="xs:integer" [1] tag="xs:string" [0..1] />
Element: Define
This element represents part of the context. The name attribute
identifies which part of the context the current element
represents. The possible values for this attribute are :
* `"B definitions"`: Definitions of predefined sets `NAT` and `INT`.
* `"ctx"`: SETS and PROPERTIES from seen components and their
included components;
* `"seext"`: INVARIANT and ASSERTIONS from seen components and
their included components;
* `"inv"`: INVARIANT of the component;
* `"ass"`: ASSERTIONS of the current component;
* `"lprp"`: SETS and PROPERTIES of the current component;
* `"inprp"`: SETS and PROPERTIES of the included components of
the current component;
* `"inext"`: INVARIANT and ASSERTIONS clauses of the included components
of the current component;
* `"cst"`: CONSTRAINTS clause of the current component;
* `"sets"`: SETS clause of the current component;
If the current component is a refinement or an implementation:
* `"mchcst"`: CONSTRAINTS clause of the component refined by
the current component;
* `"aprp"`: SETS and PROPERTIES clauses of all the refined components
as well as their included components;
* `"abs"`: INVARIANT and ASSERTIONS clauses of all the refined components
as well as their included components;
If the current component is an implementation:
* `"imlprp"`: SETS, PROPERTIES and VALUES clauses of the current component;
* `"imprp"`: SETS and PROPERTIES clauses of all the imported components
as well as their included components;
* `"imext"`: INVARIANT and ASSERTIONS clauses of all the imported
components as well as their included components.
<Define name="xs:string" [1] hash="xs:nonNegativeInteger" [1] > <Set> ... </Set> [0..*] Start Group: pred_group [0..*] Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice End Group: pred_group </Define>
<xs:element name="Define"> <xs:complexType> <xs:sequence> <xs:element ref="Set" minOccurs="0" maxOccurs="unbounded"/> <xs:group ref="pred_group" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> <xs:attribute name="name" type="xs:string" use="required"/> <xs:attribute name="hash" type="xs:nonNegativeInteger" use="required"/> </xs:complexType> </xs:element>
Element: Definition
Represents a reference to an element
[Define](#element_Define "Definition of element Define").
The attribute `name` identifies which element is referenced.
<Definition name="xs:string" [1] />
Element: EmptySeq
Represents an empty sequence.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
Element: EmptySet
Represents an empty set.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
Element: Enumerated_Values
Represents an enumeration (see element [Set](#element_Set "Description of element Set")).
* Child elements [Id](#element_Id "Description of element Id")
represent the enumerated identifiers.
Element: Exp_Comparison
Represents a comparison expression.
* Two child elements represent the arguments to the expression.
* Attribute `op` represents the operator and is restricted to
be a [comparison_op](#type_comparison_op).
<Exp_Comparison op="comparison_op" [1] > Start Group: exp_group [2..2] Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice End Group: exp_group </Exp_Comparison>
Element: Hypothesis
| Name | Hypothesis |
|---|---|
| Type | predicate_type |
| Nillable | no |
| Abstract | no |
Represents an hypothesis common to all proof obligations
in a [Proof_Obligation](#element_Proof_Obligation "Description of element Proof_Obligation").
<Hypothesis> Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice </Hypothesis>
<xs:element name="Hypothesis" type="predicate_type"/>
Element: Id
Represents the occurence of an identifier.
* Attribute `value` is the identifier.
* Optional attribute `suffix` is used for derived identifiers
and is then a positive integer. Such identifiers are created
to avoid name clashes.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<xs:element name="Id"> <xs:complexType> <xs:attribute name="value" type="xs:string" use="required"/> <xs:attribute name="suffix" type="xs:positiveInteger"/> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Integer_Literal
Represents an integer literal expression.
* Attribute `value` is the represented literal and is an
integer.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
Element: Local_Hyp
Represents an hypothesis common to some of the proof obligations
in a [Proof_Obligation](#element_Proof_Obligation "Description of element Proof_Obligation").
Attribute `num` plays the role of identifier for referencing
by individual proof obligations.
<Local_Hyp num="xs:positiveInteger" [1] > Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice </Local_Hyp>
Element: Nary_Exp
Represents a n-ary expression.
* The child elements represent the arguments.
* Attribute `op` represents the operator and shall be a
[nary_exp_op](#type_nary_exp_op).
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Nary_Exp op="nary_exp_op" [1] typref="xs:integer" [1] tag="xs:string" [0..1] > Start Group: exp_group [1..*] Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice End Group: exp_group </Nary_Exp>
<xs:element name="Nary_Exp"> <xs:complexType> <xs:group ref="exp_group" minOccurs="1" maxOccurs="unbounded"/> <xs:attribute name="op" type="nary_exp_op" use="required"/> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Nary_Pred
Represents a n-ary predicate.
* The child elements represent the arguments of the predicate.
* Attribute op represents the operator and shall be a
[nary_pred_op](#type_nary_pred_op).
<Nary_Pred op="nary_pred_op" [0..1] > Start Group: pred_group [0..*] Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice End Group: pred_group </Nary_Pred>
<xs:element name="Nary_Pred"> <xs:complexType> <xs:group ref="pred_group" minOccurs="0" maxOccurs="unbounded"/> <xs:attribute name="op" type="nary_pred_op"/> </xs:complexType> </xs:element>
Element: Proof_Obligation
This element represents a group of proof obligations.
* Child element [Tag](#element_Tag "Definition of element Tag")
contains an informational description of the source of this
group of proof obligations.
* Child elements [Definition](#element_Definition "Description of Definition elements")
reference elements of the context.
* Child elements [Hypothesis](#element_Hypothesis "Description of Hypothesis elements")
represent hypotheses that are common to all the proof obligations in this group.
* Child elements [Local_Hyp](#element_Local_Hyp "Description of Local_Hyp elements")
represent hypotheses that are common to some of the proof obligations in this group.
* Finally, child elements [Simple_Goal](#element_Simple_Goal "Description of Simple_Goal elements")
represent the proof obligations in this group.
<Proof_Obligation goalHash="xs:nonNegativeInteger" [1] > <Tag> xs:string </Tag> [1] <Definition> ... </Definition> [0..*] <Hypothesis> ... </Hypothesis> [0..*] <Local_Hyp> ... </Local_Hyp> [0..*] <Simple_Goal> ... </Simple_Goal> [0..*] </Proof_Obligation>
<xs:element name="Proof_Obligation"> <xs:complexType> <xs:sequence> <xs:element name="Tag" type="xs:string" minOccurs="1" maxOccurs="1"/> <xs:element ref="Definition" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="Hypothesis" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="Local_Hyp" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="Simple_Goal" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> <xs:attribute name="goalHash" type="xs:nonNegativeInteger" use="required"/> </xs:complexType> </xs:element>
Element: Proof_Obligations
All proof obligations in a component reference sets of
hypotheses originating from different clauses of the current
component, and of components referenced from the current
component. These references compose the _context_ of the
proof obligations.
So, in a POG file, the context is split into several sets of
hypotheses, according to their origin in the source
components. Such sets of hypotheses are represented by root
child elements named [Define](#element_Define "Definition of element Define").
Proof obligations are grouped according to their origin in
the component. For instance, the following component clauses give rise to
one group of proof obligations :
* for the initialisation;
* for each operation;
* for the well-definedness of each clause of the component
containing expressions;
In a POG file, such groups are represented by root child elements
named [Proof_Obligation](#element_Proof_Obligation "Definition of element Proof_Obligation").
Finally, typing information of expression is represented in a root
child element named [TypeInfos](#element_TypeInfos "Definition of element TypeInfos").
<Proof_Obligations version="version_type" [1] > <Define> ... </Define> [0..*] <Proof_Obligation> ... </Proof_Obligation> [0..*] <TypeInfos> ... </TypeInfos> [0..1] </Proof_Obligations>
<xs:element name="Proof_Obligations"> <xs:complexType> <xs:sequence> <xs:element ref="Define" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="Proof_Obligation" minOccurs="0" maxOccurs="unbounded"/> <xs:element ref="TypeInfos" minOccurs="0" maxOccurs="1"/> </xs:sequence> <xs:attribute name="version" type="version_type" use="required"/> </xs:complexType> </xs:element>
Element: Proof_State
Deprecated (to be removed).
Element: Quantified_Exp
Represents a quantifying expression: either a lambda-expression,
or a quantified sum or product, or a quantified union or
intersection.
* Child `Variables` is a [variables_type](#type_variables_type)
and represents the list of quantified variables.
* Child `Pred` is a [predicate_type](#type_predicate_type)
and represents the typing and otherwise constraining
predicate.
* Child element `Body` is the quantified expression;
it is of type [expression_type](#type_expression_type).
* Attribute `type` represents the operator and shall be a
[quantified_exp_op](#type_quantified_exp_op).
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Quantified_Exp type="quantified_exp_op" [1] typref="xs:integer" [1] tag="xs:string" [0..1] > <Variables> variables_type </Variables> [1] <Pred> predicate_type </Pred> [1] <Body> expression_type </Body> [1] </Quantified_Exp>
<xs:element name="Quantified_Exp"> <xs:complexType> <xs:sequence> <xs:element name="Variables" type="variables_type"/> <xs:element name="Pred" type="predicate_type"/> <xs:element name="Body" type="expression_type"/> </xs:sequence> <xs:attribute name="type" type="quantified_exp_op" use="required"/> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Quantified_Pred
Represents a quantification predicate
* Child element `Variables` represents the list of quantified variables
and is of type [variables_type](#type_variables_type).
* Child element `Body` represents the quantified predicate;
it is of type [predicate_type](#type_predicate_type).
* Attribute `type` represents the quantifier and shall be
a [quantified_pred_op](#type_quantified_pred_op).
<Quantified_Pred type="quantified_pred_op" [1] > <Variables> variables_type </Variables> [1] <Body> predicate_type </Body> [1] </Quantified_Pred>
<xs:element name="Quantified_Pred"> <xs:complexType> <xs:sequence> <xs:element name="Variables" type="variables_type"/> <xs:element name="Body" type="predicate_type"/> </xs:sequence> <xs:attribute name="type" type="quantified_pred_op" use="required"/> </xs:complexType> </xs:element>
Element: Quantified_Set
Represents a set defined in comprehension.
* Child `Variables` is a [variables_type](#type_variables_type)
and represents variables appearing in the comprehension list.
* Child `Body` is a [predicate_type](#type_predicate_type)
and represents the predicate characterizing the set elements.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Quantified_Set typref="xs:integer" [1] tag="xs:string" [0..1] > <Variables> variables_type </Variables> [1] <Body> predicate_type </Body> [1] </Quantified_Set>
<xs:element name="Quantified_Set"> <xs:complexType> <xs:sequence> <xs:element name="Variables" type="variables_type"/> <xs:element name="Body" type="predicate_type"/> </xs:sequence> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Real_Literal
Represents a real number literal expression.
* Attribute `value` is the represented literal and is a decimal
(e.g., `value="3.1415"`).
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
Element: Record
Represents a record in extension, as described in [BLRM, §5.9].
* Children `Record_Item` are
[record_item_type](#type_record_item_type)
elements and represent the different fields in the
expression.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Record typref="xs:integer" [1] tag="xs:string" [0..1] > <Record_Item> record_item_type </Record_Item> [1..*] </Record>
<xs:element name="Record"> <xs:complexType> <xs:sequence> <xs:element name="Record_Item" type="record_item_type" minOccurs="1" maxOccurs="unbounded"/> </xs:sequence> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Record_Field_Access
Represents the value of a field in a record.
* Child element represents the record.
<Record_Field_Access typref="xs:integer" [1] label="xs:string" [1] tag="xs:string" [0..1] > Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice </Record_Field_Access>
<xs:element name="Record_Field_Access"> <xs:complexType> <xs:group ref="exp_group" minOccurs="1" maxOccurs="1"/> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="label" type="xs:string" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Record_Update
Represents an updated record. Such expressions are introduced
during normalization of a "becomes equal" substitution where
the target is the field of a record, to a "becomes equal"
substitution where the target is a whole record.
For instance
```
point'xx := point'xx + 1
```
is normalized to
```
point := record_update(point, xx, point'xx + 1)
```
* The first element represents the target record.
* The attribute 'label' represents the target field.
* The last element represents the source expression.
* Optional attribute `tag` represents the position of the
expression(s) in the source code.
<Record_Update label="xs:string" [1] tag="xs:string" [0..1] > Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice </Record_Update>
Element: Ref_Hyp
Represents the reference to a local hypothesis in a proof obligation.
The value of attribute `num`
identifies the referenced hypothesis.
<Ref_Hyp num="xs:positiveInteger" [1] />
Element: STRING_Literal
Represents a string literal expression.
* Attribute `value` is the represented literal and is a string.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
Element: Set
Represents the definition of a set (in the SETS clause of a component).
* Child element [Id](#element_Id "Description of element Id") represents
the set identifier.
* If there are no child elements
[Enumerated_Values](#element_Enumerated_Values),
then it is an abstract set, otherwise it is an enumeration.
<Set> <Id> ... </Id> [1] <Enumerated_Values> ... </Enumerated_Values> [0..1] </Set>
Element: Simple_Goal
Represents an individual proof obligation in a [Proof_Obligation](#element_Proof_Obligation "Description of element Proof_Obligation") group.
* Child element Tag contains an informational text describing the role of the proof obligation.
* Child elements [Ref_Hyp](#element_Ref_Hyp "Description of element Ref_Hyp") are
references to [Local_Hyp](#element_Local_Hyp "Description of element Local_Hyp")
elements, representing hypotheses local to the current group.
* Child element Goal contains the goal predicate of the proof obligation.
* Child element [Proof_State](#element_Proof_State "Description of element Proof_State") is obsolete.
<Simple_Goal> <Tag> xs:string </Tag> [1] <Ref_Hyp> ... </Ref_Hyp> [0..*] <Goal> predicate_type </Goal> [0..1] <Proof_State> ... </Proof_State> [0..1] </Simple_Goal>
<xs:element name="Simple_Goal"> <xs:complexType> <xs:sequence> <xs:element name="Tag" type="xs:string"/> <xs:element ref="Ref_Hyp" minOccurs="0" maxOccurs="unbounded"/> <xs:element name="Goal" type="predicate_type" minOccurs="0"/> <xs:element ref="Proof_State" minOccurs="0"/> </xs:sequence> </xs:complexType> </xs:element>
Element: Struct
Represents a set of records, as described in [BLRM, §5.9].
* Children `Record_Item` are
[record_item_type](#type_record_item_type)
elements and represent the different fields in the
expression.
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Struct typref="xs:integer" [1] tag="xs:string" [0..1] > <Record_Item> record_item_type </Record_Item> [1..*] </Struct>
<xs:element name="Struct"> <xs:complexType> <xs:sequence> <xs:element name="Record_Item" type="record_item_type" minOccurs="1" maxOccurs="unbounded"/> </xs:sequence> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: Ternary_Exp
Represents a ternary expression.
* Three child elements represent the arguments.
* Attribute `op` represents the operator and shall be a
[ternary_exp_op](#type_ternary_exp_op).
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Ternary_Exp op="ternary_exp_op" [1] typref="xs:integer" [1] tag="xs:string" [0..1] > Start Group: exp_group [3..3] Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice End Group: exp_group </Ternary_Exp>
<xs:element name="Ternary_Exp"> <xs:complexType> <xs:group ref="exp_group" minOccurs="3" maxOccurs="3"/> <xs:attribute name="op" type="ternary_exp_op" use="required"/> <xs:attribute name="typref" type="xs:integer" use="required"/> <xs:attribute name="tag" type="xs:string" use="optional"/> </xs:complexType> </xs:element>
Element: TypeInfos
This is the element containing all the types of the expressions
appearing in the proof obligations.
Each child `Type` is a [typeinfos_type](#type_typeinfos_type) element
and represents a B type.
<TypeInfos> <Type> typeinfos_type </Type> [0..*] </TypeInfos>
Element: Unary_Exp
Represents a unary expression.
* The single child element represents the argument.
* Attribute `op` represents the operator and shall be a
[unary_exp_op](#type_unary_exp_op).
* Attribute `typref` is the index of the type representation
in the [TypeInfos](#element_TypeInfos) element of the document.
* Optional attribute `tag` represents a position or a list of positions
in the source bxml. It can be used to trace the origin of the expression.
<Unary_Exp op="unary_exp_op" [1] typref="xs:integer" [1] tag="xs:string" [0..1] > Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice </Unary_Exp>
Element: Unary_Pred
Represents a unary predicate.
* The single child element represent the arguments to the predicate.
* Attribute op represents the operator and shall be a
[unary_pred_op](#type_unary_pred_op).
<Unary_Pred op="unary_pred_op" [1] > Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice </Unary_Pred>
<xs:element name="Unary_Pred"> <xs:complexType> <xs:group ref="pred_group"/> <xs:attribute name="op" type="unary_pred_op" use="required"/> </xs:complexType> </xs:element>
Global Definitions
Complex Type: expression_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | expression_type |
|---|---|
| Abstract | no |
No documentation provided.
<...> Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice </...>
Complex Type: predicate_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | predicate_type |
|---|---|
| Abstract | no |
No documentation provided.
<...> Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice </...>
<xs:complexType name="predicate_type"> <xs:group ref="pred_group"/> </xs:complexType>
Complex Type: record_item_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | record_item_type |
|---|---|
| Abstract | no |
Represents a field in a record or a set of record
expression (BLRM,§5.9).
* Attribute `label` is the field identifier.
* The child represents the field expression and is
an element in [exp_group](#group_exp_group).
<... label="xs:string" [1] > Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice </...>
Complex Type: typeinfos_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | typeinfos_type |
|---|---|
| Abstract | no |
The elements representing entries in the
[TypeInfos](#element_TypeInfos) of the document.
Integer attribute `id` identifies uniquely the
type expression and is used in type references
for elements representing expressions.
<... id="xs:integer" [1] > Start Choice [1] <Binary_Exp op="*" [1] > [1] Circular model group reference: type_group [2..2] </Binary_Exp> <Id value="xs:string" [1] /> [1] <Unary_Exp op="POW" [1] > [1] Circular model group reference: type_group [1] </Unary_Exp> <Struct > [1] <Record_Item label="xs:string" [1] > [1..*] Circular model group reference: type_group [1] </Record_Item> </Struct> <Generic_Type/> [1] End Choice </...>
Complex Type: variables_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | variables_type |
|---|---|
| Abstract | no |
Represents a list of quantified identifiers, each being
a child element [Id](#element_Id).
Model Group: exp_group
| Name | exp_group |
|---|
The different types of elements representing expressions.
Start Choice [1] <Unary_Exp> ... </Unary_Exp> [1] <Binary_Exp> ... </Binary_Exp> [1] <Ternary_Exp> ... </Ternary_Exp> [1] <Nary_Exp> ... </Nary_Exp> [1] <Boolean_Literal> ... </Boolean_Literal> [1] <Boolean_Exp> ... </Boolean_Exp> [1] <EmptySet> ... </EmptySet> [1] <EmptySeq> ... </EmptySeq> [1] <Id> ... </Id> [1] <Integer_Literal> ... </Integer_Literal> [1] <Quantified_Exp> ... </Quantified_Exp> [1] <Quantified_Set> ... </Quantified_Set> [1] <STRING_Literal> ... </STRING_Literal> [1] <Struct> ... </Struct> [1] <Record> ... </Record> [1] <Real_Literal> ... </Real_Literal> [1] <Record_Update> ... </Record_Update> [1] <Record_Field_Access> ... </Record_Field_Access> [1] End Choice
<xs:group name="exp_group"> <xs:choice> <xs:element ref="Unary_Exp"/> <xs:element ref="Binary_Exp"/> <xs:element ref="Ternary_Exp"/> <xs:element ref="Nary_Exp"/> <xs:element ref="Boolean_Literal"/> <xs:element ref="Boolean_Exp"/> <xs:element ref="EmptySet"/> <xs:element ref="EmptySeq"/> <xs:element ref="Id"/> <xs:element ref="Integer_Literal"/> <xs:element ref="Quantified_Exp"/> <xs:element ref="Quantified_Set"/> <xs:element ref="STRING_Literal"/> <xs:element ref="Struct"/> <xs:element ref="Record"/> <xs:element ref="Real_Literal"/> <xs:element ref="Record_Update"/> <xs:element ref="Record_Field_Access"/> </xs:choice> </xs:group>
Model Group: pred_group
| Name | pred_group |
|---|
The different types of elements representing predicates.
Start Choice [1] <Binary_Pred> ... </Binary_Pred> [1] <Exp_Comparison> ... </Exp_Comparison> [1] <Quantified_Pred> ... </Quantified_Pred> [1] <Unary_Pred> ... </Unary_Pred> [1] <Nary_Pred> ... </Nary_Pred> [1] End Choice
<xs:group name="pred_group"> <xs:choice> <xs:element ref="Binary_Pred"/> <xs:element ref="Exp_Comparison"/> <xs:element ref="Quantified_Pred"/> <xs:element ref="Unary_Pred"/> <xs:element ref="Nary_Pred"/> </xs:choice> </xs:group>
Model Group: type_group
| Name | type_group |
|---|
Represents a B type (BLRM,§3.2).
The following representations exist:
* `Binary_Exp` to represent a Cartesian product type.
* `Unary_Exp` to represent a powerset type.
* `Struct` to represent a record type.
* `Id` to represent either a predefined type or a deferred set.
* `Generic_Type` for expression that could not be given a B type
(e.g. an empty set expression may have type `<Unary_Exp op="POW"><Generic_Type/></Unary_Exp>`).
Start Choice [1] <Binary_Exp op="*" [1] > [1] Circular model group reference: type_group [2..2] </Binary_Exp> <Id value="xs:string" [1] /> [1] <Unary_Exp op="POW" [1] > [1] Circular model group reference: type_group [1] </Unary_Exp> <Struct > [1] <Record_Item label="xs:string" [1] > [1..*] Circular model group reference: type_group [1] </Record_Item> </Struct> <Generic_Type/> [1] End Choice
<xs:group name="type_group"> <xs:choice> <xs:element name="Binary_Exp"> <xs:complexType> <xs:group ref="type_group" minOccurs="2" maxOccurs="2"/> <xs:attribute name="op" type="xs:string" use="required" fixed="*"/> </xs:complexType> </xs:element> <xs:element name="Id"> <xs:complexType> <xs:attribute name="value" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Unary_Exp"> <xs:complexType> <xs:group ref="type_group"/> <xs:attribute name="op" type="xs:string" use="required" fixed="POW"/> </xs:complexType> </xs:element> <xs:element name="Struct"> <xs:complexType> <xs:sequence> <xs:element name="Record_Item" minOccurs="1" maxOccurs="unbounded"> <xs:complexType> <xs:group ref="type_group"/> <xs:attribute name="label" type="xs:string" use="required"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Generic_Type"> <xs:complexType/> </xs:element> </xs:choice> </xs:group>
Simple Type: binary_exp_op
| Super-types: | xs:string < binary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | binary_exp_op |
|---|---|
| Content |
|
Represents the possible binary expression operators. The meaning
of the operators is described in (BLRM,§A).
Overloaded B operators are resolved :
* `*` is resolved to `"*s"` (Cartesian product),
`"*i"` (multiplication of integers),
`"*r"` (multiplication of real numbers),
`"*f"` (multiplication of floating point numbers).
* `**` is resolved to `"*s"` (Cartesian product),
`"**i"` (exponentiation of integers),
`"**r"` (exponentiation of a real numbers).
* `"+"` is resolved to
`"+i"` (addition of integers),
`"+r"` (addition of real numbers),
`"+f"` (addition of floating point numbers).
* `-` is resolved to `"-s"` (set difference),
`"-i"` (subtraction of integers),
`"-r"` (subtraction of real numbers),
`"-f"` (subtraction of floating point numbers).
* `/` is resolved to
`"/i"` (division quotient of integers),
`"/r"` (division of real numbers),
`"/f"` (division of floating point numbers).
<xs:simpleType name="binary_exp_op"> <xs:restriction base="xs:string"> <xs:enumeration value=","/> <xs:enumeration value="*"/> <xs:enumeration value="*i"/> <xs:enumeration value="*r"/> <xs:enumeration value="*f"/> <xs:enumeration value="*s"/> <xs:enumeration value="**"/> <xs:enumeration value="**i"/> <xs:enumeration value="**r"/> <xs:enumeration value="+"/> <xs:enumeration value="+i"/> <xs:enumeration value="+r"/> <xs:enumeration value="+f"/> <xs:enumeration value="+->"/> <xs:enumeration value="+->>"/> <xs:enumeration value="-"/> <xs:enumeration value="-i"/> <xs:enumeration value="-r"/> <xs:enumeration value="-f"/> <xs:enumeration value="-s"/> <xs:enumeration value="-->"/> <xs:enumeration value="-->>"/> <xs:enumeration value="->"/> <xs:enumeration value=".."/> <xs:enumeration value="/"/> <xs:enumeration value="/i"/> <xs:enumeration value="/r"/> <xs:enumeration value="/f"/> <xs:enumeration value="/\"/> <xs:enumeration value="/|\"/> <xs:enumeration value=";"/> <xs:enumeration value="<+"/> <xs:enumeration value="<->"/> <xs:enumeration value="<-"/> <xs:enumeration value="<<|"/> <xs:enumeration value="<|"/> <xs:enumeration value=">+>"/> <xs:enumeration value=">->"/> <xs:enumeration value=">+>>"/> <xs:enumeration value=">->>"/> <xs:enumeration value="><"/> <xs:enumeration value="||"/> <xs:enumeration value="\/"/> <xs:enumeration value="\|/"/> <xs:enumeration value="^"/> <xs:enumeration value="mod"/> <xs:enumeration value="|->"/> <xs:enumeration value="|>"/> <xs:enumeration value="|>>"/> <xs:enumeration value="["/> <xs:enumeration value="("/> <xs:enumeration value="<'"/> <xs:enumeration value="prj1"/> <xs:enumeration value="prj2"/> <xs:enumeration value="iterate"/> <xs:enumeration value="const"/> <xs:enumeration value="rank"/> <xs:enumeration value="father"/> <xs:enumeration value="subtree"/> <xs:enumeration value="arity"/> </xs:restriction> </xs:simpleType>
Simple Type: binary_pred_op
| Super-types: | xs:string < binary_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | binary_pred_op |
|---|---|
| Content |
|
Represents the possible values of a binary predicate operator.
They correspond to implication (`"=>"`) and equivalence (`"<=>"`) .
Simple Type: boolean_literal_type
| Super-types: | xs:string < boolean_literal_type (by restriction) |
|---|---|
| Sub-types: | None |
| Name | boolean_literal_type |
|---|---|
| Content |
|
Restricts the possible values of a Boolean literal.
Simple Type: comparison_op
| Super-types: | xs:string < comparison_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | comparison_op |
|---|---|
| Content |
|
Represents the possible values of a comparison operator. The meaning
of the operators is described in (BLRM,§A).
Some overloaded B operators are resolved :
* `>` (greater than) is resolved to
`">i"` (integers),
`">r"` (real numbers),
`">f"` (floating point numbers).
* `>=` (greater than or equal to) is resolved to
`">=i"` (integers),
`">=r"` (real numbers),
`">=f"` (floating point numbers).
* `<` (lower than) is resolved to
`"<i"` (integers),
`"<r"` (real numbers),
`"<f"` (floating point numbers).
* `<=` (lower than or equal to) is resolved to
`"<=i"` (integers),
`"<=r"` (real numbers),
`"<=f"` (floating point numbers).
<xs:simpleType name="comparison_op"> <xs:restriction base="xs:string"> <xs:enumeration value=":"/> <xs:enumeration value="/:"/> <xs:enumeration value="<:"/> <xs:enumeration value="/<:"/> <xs:enumeration value="<<:"/> <xs:enumeration value="/<<:"/> <xs:enumeration value="="/> <xs:enumeration value="/="/> <-- integer comparison --> <xs:enumeration value=">=i"/> <xs:enumeration value=">i"/> <xs:enumeration value="<i"/> <xs:enumeration value="<=i"/> <-- real comparison --> <xs:enumeration value=">=r"/> <xs:enumeration value=">r"/> <xs:enumeration value="<r"/> <xs:enumeration value="<=r"/> <-- float comparison --> <xs:enumeration value=">=f"/> <xs:enumeration value=">f"/> <xs:enumeration value="<f"/> <xs:enumeration value="<=f"/> </xs:restriction> </xs:simpleType>
Simple Type: nary_exp_op
| Super-types: | xs:string < nary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | nary_exp_op |
|---|---|
| Content |
|
Represents the possible n-ary expression operators:
* `"["` is used to represent a sequence literal.
* `"{"` is used to represent a set literal defined in extension.
Simple Type: nary_pred_op
| Super-types: | xs:string < nary_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | nary_pred_op |
|---|---|
| Content |
|
Represents the possible n-ary predicate operators : conjunction
(`"&"`) and disjunction (`"or"`).
Simple Type: quantified_exp_op
| Super-types: | xs:string < quantified_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | quantified_exp_op |
|---|---|
| Content |
|
Represents the possible expression quantifiers. The meaning
of the quantifiers is described in (BLRM,§A).
Overloaded B operators are resolved :
* `SIGMA` is resolved to
`"iSIGMA"` (sum over integers),
`"rSIGMA"` (sum over real numbers).
* `PI` is resolved to
`"iPI"` (product over integers),
`"rPI"` (product over real numbers).
<xs:simpleType name="quantified_exp_op"> <xs:restriction base="xs:string"> <xs:enumeration value="%"/> <xs:enumeration value="SIGMA"/> <xs:enumeration value="iSIGMA"/> <xs:enumeration value="rSIGMA"/> <xs:enumeration value="PI"/> <xs:enumeration value="iPI"/> <xs:enumeration value="rPI"/> <xs:enumeration value="INTER"/> <xs:enumeration value="UNION"/> </xs:restriction> </xs:simpleType>
Simple Type: quantified_pred_op
| Super-types: | xs:string < quantified_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | quantified_pred_op |
|---|---|
| Content |
|
Represents the possible quantifiers:
`"!"` for universal and `"#"` for existential.
Simple Type: ternary_exp_op
| Super-types: | xs:string < ternary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | ternary_exp_op |
|---|---|
| Content |
|
Represents the possible ternary expression operators. The meaning
of the operators is described in (BLRM,§A).
Simple Type: unary_exp_op
| Super-types: | xs:string < unary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | unary_exp_op |
|---|---|
| Content |
|
Represents the possible unary expression operators. The meaning
of the operators is described in (BLRM,§A).
Overloaded B operators are resolved :
* `max` is resolved to
`"imax"` (maximum of a set of integers),
`"rmax"` (maximum of a set of real numbers).
* `min` is resolved to
`"imin"` (minimum of a set of integers),
`"rmin"` (minimum of a set of real numbers).
* `-` (unary minus) is resolved to
`"-i"` (unary minus over integers),
`"-r"` (unary minus over real numbers).
<xs:simpleType name="unary_exp_op"> <xs:restriction base="xs:string"> <xs:enumeration value="max"/> <xs:enumeration value="imax"/> <xs:enumeration value="rmax"/> <xs:enumeration value="min"/> <xs:enumeration value="imin"/> <xs:enumeration value="rmin"/> <xs:enumeration value="card"/> <xs:enumeration value="dom"/> <xs:enumeration value="ran"/> <xs:enumeration value="POW"/> <xs:enumeration value="POW1"/> <xs:enumeration value="FIN"/> <xs:enumeration value="FIN1"/> <xs:enumeration value="union"/> <xs:enumeration value="inter"/> <xs:enumeration value="seq"/> <xs:enumeration value="seq1"/> <xs:enumeration value="iseq"/> <xs:enumeration value="iseq1"/> <xs:enumeration value="-"/> <xs:enumeration value="-i"/> <xs:enumeration value="-r"/> <xs:enumeration value="~"/> <xs:enumeration value="size"/> <xs:enumeration value="perm"/> <xs:enumeration value="first"/> <xs:enumeration value="last"/> <xs:enumeration value="id"/> <xs:enumeration value="closure"/> <xs:enumeration value="closure1"/> <xs:enumeration value="tail"/> <xs:enumeration value="front"/> <xs:enumeration value="rev"/> <xs:enumeration value="conc"/> <xs:enumeration value="succ"/> <xs:enumeration value="pred"/> <xs:enumeration value="rel"/> <xs:enumeration value="fnc"/> <xs:enumeration value="real"/> <xs:enumeration value="floor"/> <xs:enumeration value="ceiling"/> <xs:enumeration value="tree"/> <xs:enumeration value="btree"/> <xs:enumeration value="top"/> <xs:enumeration value="sons"/> <xs:enumeration value="prefix"/> <xs:enumeration value="postfix"/> <xs:enumeration value="sizet"/> <xs:enumeration value="mirror"/> <xs:enumeration value="left"/> <xs:enumeration value="right"/> <xs:enumeration value="infix"/> <xs:enumeration value="bin"/> </xs:restriction> </xs:simpleType>
Simple Type: unary_pred_op
| Super-types: | xs:string < unary_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | unary_pred_op |
|---|---|
| Content |
|
Represents the possible operators:
`"not"` (for negation) is the only possibility.
Simple Type: version_type
| Super-types: | xs:string < version_type (by restriction) |
|---|---|
| Sub-types: | None |
| Name | version_type |
|---|---|
| Content |
|
Represents the possible values for the `version` attribute for
the root element. Currently a unique value is possible: `"1.0"`.
When the format evolves, the new versions will be added there.
Glossary
Abstract (Applies to complex type definitions and element declarations). An abstract element or complex type cannot used to validate an element instance. If there is a reference to an abstract element, only element declarations that can substitute the abstract element can be used to validate the instance. For references to abstract type definitions, only derived types can be used.
All Model Group Child elements can be provided in any order in instances. See: http://www.w3.org/TR/xmlschema-1/#element-all.
Choice Model Group Only one from the list of child elements and model groups can be provided in instances. See: http://www.w3.org/TR/xmlschema-1/#element-choice.
Collapse Whitespace Policy Replace tab, line feed, and carriage return characters with space character (Unicode character 32). Then, collapse contiguous sequences of space characters into single space character, and remove leading and trailing space characters.
Disallowed Substitutions (Applies to element declarations). If substitution is specified, then substitution group members cannot be used in place of the given element declaration to validate element instances. If derivation methods, e.g. extension, restriction, are specified, then the given element declaration will not validate element instances that have types derived from the element declaration's type using the specified derivation methods. Normally, element instances can override their declaration's type by specifying an xsi:type attribute.
Key Constraint Like Uniqueness Constraint, but additionally requires that the specified value(s) must be provided. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.
Key Reference Constraint Ensures that the specified value(s) must match value(s) from a Key Constraint or Uniqueness Constraint. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.
Model Group Groups together element content, specifying the order in which the element content can occur and the number of times the group of element content may be repeated. See: http://www.w3.org/TR/xmlschema-1/#Model_Groups.
Nillable (Applies to element declarations). If an element declaration is nillable, instances can use the xsi:nil attribute. The xsi:nil attribute is the boolean attribute, nil, from the http://www.w3.org/2001/XMLSchema-instance namespace. If an element instance has an xsi:nil attribute set to true, it can be left empty, even though its element declaration may have required content.
Notation A notation is used to identify the format of a piece of data. Values of elements and attributes that are of type, NOTATION, must come from the names of declared notations. See: http://www.w3.org/TR/xmlschema-1/#cNotation_Declarations.
Preserve Whitespace Policy Preserve whitespaces exactly as they appear in instances.
Prohibited Derivations (Applies to type definitions). Derivation methods that cannot be used to create sub-types from a given type definition.
Prohibited Substitutions (Applies to complex type definitions). Prevents sub-types that have been derived using the specified derivation methods from validating element instances in place of the given type definition.
Replace Whitespace Policy Replace tab, line feed, and carriage return characters with space character (Unicode character 32).
Sequence Model Group Child elements and model groups must be provided in the specified order in instances. See: http://www.w3.org/TR/xmlschema-1/#element-sequence.
Substitution Group Elements that are members of a substitution group can be used wherever the head element of the substitution group is referenced.
Substitution Group Exclusions (Applies to element declarations). Prohibits element declarations from nominating themselves as being able to substitute a given element declaration, if they have types that are derived from the original element's type using the specified derivation methods.
Target Namespace The target namespace identifies the namespace that components in this schema belongs to. If no target namespace is provided, then the schema components do not belong to any namespace.
Uniqueness Constraint Ensures uniqueness of an element/attribute value, or a combination of values, within a specified scope. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.