- Add an eager and lazy invariants checking functions mechanism
for low level invariants to allow the checking of invariants
only when opening or closing a monitor instance.
The state of the monitor instances traces evolves when declaring
instances between open_monitor* and close_monitor* commands.
This mechanism can capture the changes be defining
invariants before or after traces are populated but not
before and after, with the current mechanism.
Two tables were added: docclass_eager_inv_tab
and docclass_lazy_inv_tab to store these invariants
- Implement CENELEC_50128 Table A.1 using this mechanism
- Update phase datatype to be accurate with 7.3 in the standard
- Update cenelec_document class: according to the table C.1 in the
standard, written by, first check, and second check can be optional.
See Phase Planning line 4 in the table, for example
- Some specifications are external to the standard: implement them
as external_specification subclasses
- Fix phases attributes of classes
- Warning: the current implementation does yet not support
some use-cases, like invariant on monitors,
or the initialization of docitem without a class associated.
- Add first draft of the checking of invariants.
For now, it is disabled by default because some cases
are not yet supported, like the initialization of docitem
without a class associated.
ex: text*[sdf]‹ Lorem ipsum @{thm refl}›
- To enable the checking, one can use the theory attribute
"invariants_checking" by declaring it in a theory like this:
declare [[invariants_strict_checking = true]]
- A checking using basic tactics (unfolding and auto) can be enable
with the "invariants_checking_with_tactics" theory attribute
for specific use-cases
- The specification of invariants is now automatically abstracted,
so one must define an invariant like this now:
doc_class W =
w::"int"
invariant w :: "w σ ≥ 3"
The old form:
doc_class W =
w::"int"
invariant w :: "λσ. w σ ≥ 3"
is now deprecated.
The specification of the invariant still uses the σ-notation
and is defined globally by the name component "invariantN"
- Update the invariants definition in the theories to match
the new implementation
- Update the manual to explain this new feature
- Add small examples in src/tests/High_Level_Syntax_Invariants.thy
and src/tests/Ontology_Matching_Example.thy
- Add a new Term Annotation Antiquotation (TA)
to allow requests on instances.
Example:
@{C-instances} will return all the instances of the class "C"
defined in the generated theory
- Update ISA_transformers elaborate function signature to
take into account the case where the term argument
of a TA is irrelevant, for example when a TA has no argument.
Example with the TA of the instances of a class:
@{A-instances}
Here the TA has no argument and none second level type checking is
wished, so its associated check function can be the identity function
with respect to the ISA_transformers chek function type.
- Add some request examples in Evaluation.thy
- Fix typos
- Fix the generation of the record associated with
a class and used for the logic.
The old implementation generated a new attribute
for each attribute defined by a subclass,
even the ones that were overriding ones of the superclass.
The new implementation generates the attributes of the subclass
which are not overriding ones.
Warning:
It implies that overridden attributes in a subclass are not
new attributes added to the theory context.
So the base name of an attribute will refer to the attribute
of the last declared class where it is defined.
If ones wants to refer to atttributes, one should use
long names, even in the invariants of a subclass definition
which overrides the attribute used in the invariant.
For example,
in ~~/src/ontologies/scholarly_paper/scholarly_paper.thy:
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
status :: status <= "description"
formal_results :: "thm list"
invariant L1 :: "λσ::technical. the (level σ) > 0"
type_synonym tc = technical (* technical content *)
doc_class example = text_section +
referentiable :: bool <= True
status :: status <= "description"
short_name :: string <= "''''"
doc_class math_content = tc +
referentiable :: bool <= True
short_name :: string <= "''''"
status :: status <= "semiformal"
mcc :: "math_content_class" <= "thm"
invariant s1 :: "λ σ::math_content. ¬referentiable σ ⟶ short_name σ = ''''"
invariant s2 :: "λ σ::math_content. technical.status σ = semiformal"
The class math_content overrride the attribute status
of the class technical, by using the type synonym tc,
but the base name of this attribute refers
to the attribute of the class example where it is last defined
and not just overridden.
So in the invariant s2 of the class math_content,
we must use the long name of the attribute,
i.e. the base name "status" with its qualifier which refers
to the superclass where it is defined, the class technical.
Type synonyms as qualifiers are not yet supported.
- Qualify classes that only override attributes of their superclass
as vitual classes by adding a virtual attribute.
This attribute is used to discriminate virtual classes and generate
an adequate make function to initialize their associated record.
The implementation uses an hidden attribute (the tag_attribute)
to force the virtual class to be concrete or the logic
by having a full new record definition associated with it.
For example:
doc_class W =
a::"int" <= "1"
doc_class X = W +
a::"int" <= "2"
The class X is tagged as a virtual class and
the record make functions of the classes W and X are:
W.make W_tag_attribute W_a
X.make X_tag_attribute X_a X_tag_attribute
So a record definition is added to the theory context for each class,
even though a virtual class only overrides
attributes of its superclass.
This behavior allows us to support definitions of new default values
for attributes in the subclass, as shown in the example.
- Factorize make name components
- Use Record name components instead of strings to refer to Record
components
- Fix typos
Burkhart Wolff
Burkhart Wolff
Achim D. Brucker
Nicolas Méric
Makarius Wenzel