|
Target Namespace
|
https://www.atelierb.eu/Formats/mechanism
|
| Element and Attribute Namespaces |
- Global element and attribute declarations belong to this schema's target namespace.
- By default, local element declarations belong to this schema's target namespace.
- By default, local attribute declarations have no namespace.
|
This schema defines the format for proof mechanisms. In Atelier
B, proof mechanisms are descriptions of how automatic proof
programs (_provers_) should be applied to proof
obligations.
* This documentation corresponds to version 1.0 of the format.
* The root element is always a [mechanism](#element_mechanism
"Definition of element mechanism").
### 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/mechanism
|
|
xml
|
http://www.w3.org/XML/1998/namespace |
|
xs
|
http://www.w3.org/2001/XMLSchema |
<xs:schema id="ProofMechanismXSD" targetNamespace="https://www.atelierb.eu/Formats/mechanism" elementFormDefault="qualified">
...
</xs:schema>
There is a unique element `mechanism` represents a proof mechanism.
It has an identifier (attribute `name`), and a trust level
(attribute `trust) specifying whether a `Proved` result shall
be trusted or not.
A proof mechanism may be composed of several provers that are
to be applied in sequence. Each prover is accessed through a
so called _driver_ (child elements `driver`, of type
[driverType](#complexType_driverType "Definition of complex type
driverType")).
For convenience, `definition` child elements may appear, to
group elements that would otherwise be repeated multiple times
in the file. They have the type
[definitionType](#complexType_definitionType "Definition of complex
type definitionType")
<xs:element name="mechanism">
<xs:complexType>
<xs:sequence>
<xs:element name="definition" type="definitionType" minOccurs="0" maxOccurs="unbounded"/>
<xs:element name="driver" type="driverType" maxOccurs="unbounded"/>
</xs:sequence>
<xs:attribute name="name" type="xs:string" use="required"/>
<xs:attribute name="trust" type="trustType" use="required"/>
</xs:complexType>
</xs:element>
| Super-types: |
None |
| Sub-types: |
None |
A `definitionType` element represents a list of command line
parameters. This list corresponds to the list of child
elements. A child element is either a `parameter` or an
`expandType` element, which shall reference another `definitionType`
element, appearing previously in the mechanism.
<xs:complexType name="definitionType">
<xs:sequence>
<xs:element name="param" type="parameterType" maxOccurs="unbounded"/>
<xs:element name="expand" type="expandType" minOccurs="0" maxOccurs="unbounded"/>
</xs:sequence>
</xs:complexType>
| Super-types: |
None |
| Sub-types: |
None |
A driver is a wrapper for a prover. In addition to executing
the prover, it is also responsible for converting between
Atelier B data formats and the inputs and outputs of the
prover.
A `driver` element has an identifier (attribute `name`),
and has three components as child elements:
* The _writer_ (child element `writer`) translates to the
input format of the prover. A writer should be a command line
program complying to the following requirements:
1. It interprets the argument `-i comp.pog` as specifying the
the path to a `pog` file, containing all the proof obligations
of a component. This argument is mandatory.
1. It interprets the option `-o comp.po2` as specifying the
the path to a file where the translation of the proof
obligations will be stored. If this option is not present, the
translation should be printed to the standard output channel.
1. It shall be able to translate either all goals or selected
goals from this file.
1. It interprets the option `-A` as the directive to translate
all the goals found in the `pog` file.
1. It interprets the option `-a i j`, where `i` is the
position of a `Proof_Obligation` element in the `pog` file,
and `j` is the position of a `Simple_Goal` child of this
element.
1. It shall be able to handle several such `-a` options.
1. Options `-A` and `-a` are mutually exclusive.
* The _prover_ (child element `prover`) itself.
* The _reader_ (child element `reader`) reads from its the
standard input the output of the prover and produces on its
standard output a sequence of proof statuses (`Proved`,
`Disproved`, `Unknown`) on its output.
Both child elements `writer` and `reader` must conform to the
`toolType` element specification, while child element `prover` is
of type `proverType`.
Finally, a driver must declare how it expects proof
obligations to be grouped, with an attribute `group` (see the
type [groupType](#simpleType_groupType "Definition of simple type
groupType") for details).
Optionnaly, it can declare a specific extension for the file
generated by the writer.
po2 is the default extension.
A driver can be declared "fast". By default, the attribute is false.
A fast driver is used in the B editor when the edited file is saved.
<xs:complexType name="driverType">
<xs:sequence>
<xs:element name="writer" type="toolType"/>
<xs:element name="prover" type="proverType"/>
<xs:element name="reader" type="toolType"/>
</xs:sequence>
<xs:attribute name="name" type="xs:string" use="required"/>
<xs:attribute name="group" type="groupType" use="required"/>
<xs:attribute name="ext" type="xs:string" use="optional"/>
<xs:attribute name="fast" type="xs:boolean" use="optional"/>
</xs:complexType>
| Super-types: |
None |
| Sub-types: |
None |
An `expandType` element has an attribute `value` that shall
be valued to the name of a `definitionType` element occurring
previously in the mechanism.
<...
value="xs:string" [1]
/>
<xs:complexType name="expandType">
<xs:attribute name="value" type="xs:string" use="required"/>
</xs:complexType>
| Super-types: |
None |
| Sub-types: |
None |
Type `param` elements define command-line parameters of programs.
These elements have three attributes: `name`, `value` and
`separator`. All attributes are optional, but either `name` or
`value` shall be present. The default value for `separator` is
`' '`.
The corresponding command line parameter is computed as follows:
* The value of attribute `name` if attribute `value` is missing.
* The value of attribute `value` if attribute `name` is missing.
* The concatenation of attributes `name`, `separator` and `value`,
in that order, otherwise.
<...
name="xs:string" [0..1]
value="xs:string" [0..1]
separator="xs:string" [0..1]
/>
<xs:complexType name="parameterType">
<xs:attribute name="name" type="xs:string" use="optional"/>
<xs:attribute name="value" type="xs:string" use="optional"/>
<xs:attribute name="separator" type="xs:string" use="optional"/>
</xs:complexType>
| Super-types: |
None |
| Sub-types: |
None |
A type `proverType` element defines the prover of a driver. Its
structure extends that of a `tool` element. It has an
identifier (attribute `name`). The path to the prover is either
given explicity with attribute `path`, or is an Atelier B
resource, specified with attribute `resource`. In case both
are present, the latter takes precedence over the former.
Command line parameters to execute the tool may be specified
with child elements `param`, of type
[parameterType](#complexType_parameterType "Definition of complex type
parameterType"), and `expand`, of type
[expandType](#complexType_expandType "Definition of complex type
expandType").
Attribute `timeout` indicates whether the prover shall be
interrupted after it has executed after the given amount (in
whole seconds). Attribute `input` states whether the prover
expects input from a file or from the standard input channel.
<...
name="xs:string" [1]
path="xs:string" [0..1]
resource="xs:string" [0..1]
input="inputType" [0..1]
timeout="xs:integer" [0..1]
>
<param> parameterType </param> [0..*]
<expand> expandType </expand> [0..*]
</...>
<xs:complexType name="proverType">
<xs:sequence>
<xs:element name="param" type="parameterType" minOccurs="0" maxOccurs="unbounded"/>
<xs:element name="expand" type="expandType" minOccurs="0" maxOccurs="unbounded"/>
</xs:sequence>
<xs:attribute name="name" type="xs:string" use="required"/>
<xs:attribute name="path" type="xs:string" use="optional"/>
<xs:attribute name="resource" type="xs:string" use="optional"/>
<xs:attribute name="input" type="inputType" use="optional"/>
<xs:attribute name="timeout" type="xs:integer" use="optional"/>
</xs:complexType>
| Super-types: |
xs:string < groupType (by restriction) |
| Sub-types: |
None |
| Name |
groupType |
| Content |
- value comes from list: {'none'|'related'|'full'}
|
A `groupType` attribute specifies how proof obligations shall be
grouped for each execution of a prover.
* Value `none` indicates that each goal will be handled in a
single execution. There will be an execution of the driver
writer, prover and reader for each such goal.
* The value `related` indicates that all the goals that are
related in the `pog` file will be handled in a single
execution of the driver. For instance, there will be one such
execution for each operation, one execution for all the
operations.
* With the value `full`, all the goals are handled in a
single execution.
<xs:simpleType name="groupType">
<xs:restriction base="xs:string">
<xs:enumeration value="none"/>
<xs:enumeration value="related"/>
<xs:enumeration value="full"/>
</xs:restriction>
</xs:simpleType>
| Super-types: |
xs:string < trustType (by restriction) |
| Sub-types: |
None |
| Name |
trustType |
| Content |
- value comes from list: {'never'|'redundancy'|'always'}
|
Trust is an attribute of a mechanism. This attribute is used
to choose how the proof status of a proof obligation goal is
set in Atelier B depending on the results of the provers.
It may take one of the following values:
* `'never'`: If a prover discharges successfully a proof
obligation, the proof status should be set to `Probably
proved`. This is the default value.
* `'always'`: If a prover discharges successfully a proof
obligation, the proof status in Atelier B should be set to
`Proved`.
* `'redundancy'`: If two provers in the mechanism discharge
successfully a proof obligation, the proof status in Atelier
B should be set to `Proved`. If only one prover is successful,
then the proof status should be set to `Probably proved`.
<xs:simpleType name="trustType">
<xs:restriction base="xs:string">
<xs:enumeration value="never"/>
<xs:enumeration value="redundancy"/>
<xs:enumeration value="always"/>
</xs:restriction>
</xs:simpleType>
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.