The Assertion Package

Overview

Assertions are expressed in archetypes in typed first-order predicate logic (FOL). They are used in two places: to express archetype slot constraints, and to express rules in complex object constraints. In both of these places, their role is to constrain something inside the archetype. Constraints on external resources such as terminologies are expressed in the constraint binding part of the archetype ontology, described in [_terminology_package]. The assertion package is illustrated below.

AM aom14.archetype.assertion
Figure 1. aom14.archetype.assertion Package

Semantics

Archetype assertions are statements which contain the following elements:

  • variables, which are inbuilt, archetype path-based, or external query results;

  • manifest constants of any primitive type, including the date/time types

  • arithmetic operators: +, *, -, /, ^ (exponent), % (modulo division)

  • relational operators: >, <, >=, <=, =, !=, matches

  • boolean operators: not, and, or, xor

  • quantifiers applied to container variables: for_all, exists

The written syntax of assertions is defined in the openEHR ADL document. The package described here is currently designed to allow the representation of a general-purpose binary expression tree, as would be generated by a parser. This may be replaced in the future by a more specific model, if needed.

This relatively simple model of expressions is sufficiently powerful for representing FOL expressions on archetype structures, although it could clearly be more heavily subtyped.

Class Descriptions

ASSERTION Class

  • Definition

  • Effective

  • BMM

  • UML

Class

ASSERTION

Description

Structural model of a typed first order predicate logic assertion, in the form of an expression tree, including optional variable definitions.

Attributes

Signature

Meaning

0..1

tag: String

Expression tag, used for differentiating multiple assertions.

0..1

string_expression: String

String form of expression, in case an expression evaluator taking String expressions is used for evaluation.

1..1

expression: EXPR_ITEM

Root of expression tree.

0..1

variables: List<ASSERTION_VARIABLE>

Definitions of variables used in the assertion expression.

Invariants

Tag_valid: tag /= Void implies not tag.is_empty

Expression_valid: expression /= Void and then expression.type.is_equal(“BOOLEAN”)
ASSERTION

Structural model of a typed first order predicate logic assertion, in the form of an expression tree, including optional variable definitions.

Attributes

tag: String [0..1]

Expression tag, used for differentiating multiple assertions.

string_expression: String [0..1]

String form of expression, in case an expression evaluator taking String expressions is used for evaluation.

expression: EXPR_ITEM [1..1]

Root of expression tree.

variables: List<ASSERTION_VARIABLE> [0..1]

Definitions of variables used in the assertion expression.

Invariants

Tag_valid: tag /= Void implies not tag.is_empty

Expression_valid: expression /= Void and then expression.type.is_equal(“BOOLEAN”)

 
{
    "name": "ASSERTION",
    "documentation": "Structural model of a typed first order predicate logic assertion, in the form of an expression tree, including optional variable definitions. ",
    "properties": {
        "tag": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "tag",
            "documentation": "Expression tag, used for differentiating multiple assertions.",
            "type": "String"
        },
        "string_expression": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "string_expression",
            "documentation": "String form of expression, in case an expression evaluator taking String expressions is used for evaluation. ",
            "type": "String"
        },
        "expression": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "expression",
            "documentation": "Root of expression tree.",
            "is_mandatory": true,
            "type": "EXPR_ITEM"
        },
        "variables": {
            "_type": "P_BMM_CONTAINER_PROPERTY",
            "name": "variables",
            "documentation": "Definitions of variables used in the assertion expression.",
            "type_def": {
                "container_type": "List",
                "type": "ASSERTION_VARIABLE"
            },
            "cardinality": {
                "lower": 0,
                "upper_unbounded": true
            }
        }
    },
    "invariants": {
        "Tag_valid": "tag /= Void implies not tag.is_empty",
        "Expression_valid": "expression /= Void and then expression.type.is_equal(“BOOLEAN”)"
    }
}
aom14.assertion

EXPR_ITEM Class

  • Definition

  • Effective

  • BMM

  • UML

Class

EXPR_ITEM (abstract)

Description

Abstract parent of all expression tree items.

Attributes

Signature

Meaning

1..1

type: String

Type name of this item in the mathematical sense. For leaf nodes, must be the name of a primitive type, or else a reference model type. The type for any relational or boolean operator will be “Boolean”, while the type for any arithmetic operator, will be “Real” or “Integer”.
EXPR_ITEM (abstract)

Abstract parent of all expression tree items.

Attributes

type: String [1..1]

Type name of this item in the mathematical sense. For leaf nodes, must be the name of a primitive type, or else a reference model type. The type for any relational or boolean operator will be “Boolean”, while the type for any arithmetic operator, will be “Real” or “Integer”.

 
{
    "name": "EXPR_ITEM",
    "documentation": "Abstract parent of all expression tree items.",
    "is_abstract": true,
    "properties": {
        "type": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "type",
            "documentation": "Type name of this item in the mathematical sense. For leaf nodes, must be the name of a primitive type, or else a reference model type. The type for any relational or boolean operator will be “Boolean”, while the type for any arithmetic operator, will be “Real” or “Integer”.",
            "is_mandatory": true,
            "type": "String"
        }
    }
}
aom14.expr item

EXPR_LEAF Class

  • Definition

  • Effective

  • BMM

  • UML

Class

EXPR_LEAF

Description

Expression tree leaf item representing one of:

  • a manifest constant of any primitive type;

  • a path referring to a value in the archetype;

  • a constraint;

  • a variable reference.

Inherit

EXPR_ITEM

Attributes

Signature

Meaning

1..1

reference_type: String

Type of reference: “constant”, “attribute”, “function”, “constraint”. The first three are used to indicate the referencing mechanism for an operand. The last is used to indicate a constraint operand, as happens in the case of the right-hand operand of the ‘matches’ operator.

1..1

item: Any

The value referred to; a manifest constant, an attribute path (in the form of a String), or for the right-hand side of a ‘matches’ node, a constraint, often a C_PRIMITIVE_OBJECT.
EXPR_LEAF

Expression tree leaf item representing one of:

  • a manifest constant of any primitive type;

  • a path referring to a value in the archetype;

  • a constraint;

  • a variable reference.

Inherits: EXPR_ITEM

Attributes

type: String [1..1]

Type name of this item in the mathematical sense. For leaf nodes, must be the name of a primitive type, or else a reference model type. The type for any relational or boolean operator will be “Boolean”, while the type for any arithmetic operator, will be “Real” or “Integer”.
Inherited from EXPR_ITEM

reference_type: String [1..1]

Type of reference: “constant”, “attribute”, “function”, “constraint”. The first three are used to indicate the referencing mechanism for an operand. The last is used to indicate a constraint operand, as happens in the case of the right-hand operand of the ‘matches’ operator.

item: Any [1..1]

The value referred to; a manifest constant, an attribute path (in the form of a String), or for the right-hand side of a ‘matches’ node, a constraint, often a C_PRIMITIVE_OBJECT.

 
{
    "name": "EXPR_LEAF",
    "documentation": "Expression tree leaf item representing one of:\n\n* a manifest constant of any primitive type;\n* a path referring to a value in the archetype;\n* a constraint;\n* a variable reference.\n",
    "ancestors": [
        "EXPR_ITEM"
    ],
    "properties": {
        "reference_type": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "reference_type",
            "documentation": "Type of reference: “constant”, “attribute”, “function”, “constraint”. The first three are used to indicate the referencing mechanism for an operand. The last is used to indicate a constraint operand, as happens in the case of the right-hand operand of the ‘matches’ operator.",
            "is_mandatory": true,
            "type": "String"
        },
        "item": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "item",
            "documentation": "The value referred to; a manifest constant, an attribute path (in the form of a String), or for the right-hand side of a ‘matches’ node, a constraint, often a C_PRIMITIVE_OBJECT.",
            "is_mandatory": true,
            "type": "Any"
        }
    }
}
aom14.expr leaf

EXPR_OPERATOR Class

  • Definition

  • Effective

  • BMM

  • UML

Class

EXPR_OPERATOR (abstract)

Description

Abstract parent of operator types.

Inherit

EXPR_ITEM

Attributes

Signature

Meaning

0..1

precedence_overridden: Boolean

True if the natural precedence of operators is overridden in the expression represented by this node of the expression tree. If True, parentheses should be introduced around the totality of the syntax expression corresponding to this operator node and its operands.

1..1

operator: OPERATOR_KIND

Code of operator.
EXPR_OPERATOR (abstract)

Abstract parent of operator types.

Inherits: EXPR_ITEM

Attributes

type: String [1..1]

Type name of this item in the mathematical sense. For leaf nodes, must be the name of a primitive type, or else a reference model type. The type for any relational or boolean operator will be “Boolean”, while the type for any arithmetic operator, will be “Real” or “Integer”.
Inherited from EXPR_ITEM

precedence_overridden: Boolean [0..1]

True if the natural precedence of operators is overridden in the expression represented by this node of the expression tree. If True, parentheses should be introduced around the totality of the syntax expression corresponding to this operator node and its operands.

operator: OPERATOR_KIND [1..1]

Code of operator.

 
{
    "name": "EXPR_OPERATOR",
    "documentation": "Abstract parent of operator types.",
    "is_abstract": true,
    "ancestors": [
        "EXPR_ITEM"
    ],
    "properties": {
        "precedence_overridden": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "precedence_overridden",
            "documentation": "True if the natural precedence of operators is overridden in the expression represented by this node of the expression tree. If True, parentheses should be introduced around the totality of the syntax expression corresponding to this operator node and its operands.",
            "type": "Boolean"
        },
        "operator": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "operator",
            "documentation": "Code of operator.",
            "is_mandatory": true,
            "type": "OPERATOR_KIND"
        }
    }
}
aom14.expr operator

EXPR_UNARY_OPERATOR Class

  • Definition

  • Effective

  • BMM

  • UML

Class

EXPR_UNARY_OPERATOR

Description

Unary operator expression node.

Inherit

EXPR_OPERATOR

Attributes

Signature

Meaning

1..1

operand: EXPR_ITEM

Operand node.
EXPR_UNARY_OPERATOR

Unary operator expression node.

Inherits: EXPR_ITEM, EXPR_OPERATOR

Attributes

type: String [1..1]

Type name of this item in the mathematical sense. For leaf nodes, must be the name of a primitive type, or else a reference model type. The type for any relational or boolean operator will be “Boolean”, while the type for any arithmetic operator, will be “Real” or “Integer”.
Inherited from EXPR_ITEM

precedence_overridden: Boolean [0..1]

True if the natural precedence of operators is overridden in the expression represented by this node of the expression tree. If True, parentheses should be introduced around the totality of the syntax expression corresponding to this operator node and its operands.
Inherited from EXPR_OPERATOR

operator: OPERATOR_KIND [1..1]

Code of operator.
Inherited from EXPR_OPERATOR

operand: EXPR_ITEM [1..1]

Operand node.

 
{
    "name": "EXPR_UNARY_OPERATOR",
    "documentation": "Unary operator expression node.",
    "ancestors": [
        "EXPR_OPERATOR"
    ],
    "properties": {
        "operand": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "operand",
            "documentation": "Operand node.",
            "is_mandatory": true,
            "type": "EXPR_ITEM"
        }
    }
}
aom14.expr unary operator

EXPR_BINARY_OPERATOR Class

  • Definition

  • Effective

  • BMM

  • UML

Class

EXPR_BINARY_OPERATOR

Description

Binary operator expression node.

Inherit

EXPR_OPERATOR

Attributes

Signature

Meaning

1..1

left_operand: EXPR_ITEM

Left operand node.

1..1

right_operand: EXPR_ITEM

Right operand node.
EXPR_BINARY_OPERATOR

Binary operator expression node.

Inherits: EXPR_ITEM, EXPR_OPERATOR

Attributes

type: String [1..1]

Type name of this item in the mathematical sense. For leaf nodes, must be the name of a primitive type, or else a reference model type. The type for any relational or boolean operator will be “Boolean”, while the type for any arithmetic operator, will be “Real” or “Integer”.
Inherited from EXPR_ITEM

precedence_overridden: Boolean [0..1]

True if the natural precedence of operators is overridden in the expression represented by this node of the expression tree. If True, parentheses should be introduced around the totality of the syntax expression corresponding to this operator node and its operands.
Inherited from EXPR_OPERATOR

operator: OPERATOR_KIND [1..1]

Code of operator.
Inherited from EXPR_OPERATOR

left_operand: EXPR_ITEM [1..1]

Left operand node.

right_operand: EXPR_ITEM [1..1]

Right operand node.

 
{
    "name": "EXPR_BINARY_OPERATOR",
    "documentation": "Binary operator expression node.",
    "ancestors": [
        "EXPR_OPERATOR"
    ],
    "properties": {
        "left_operand": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "left_operand",
            "documentation": "Left operand node.",
            "is_mandatory": true,
            "type": "EXPR_ITEM"
        },
        "right_operand": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "right_operand",
            "documentation": "Right operand node.",
            "is_mandatory": true,
            "type": "EXPR_ITEM"
        }
    }
}
aom14.expr binary operator

ASSERTION_VARIABLE Class

  • Definition

  • Effective

  • BMM

  • UML

Class

ASSERTION_VARIABLE

Description

Definition of a named variable used in an assertion expression.

Attributes

Signature

Meaning

1..1

name: String

Name of variable.

1..1

definition: String

Formal definition of the variable.
ASSERTION_VARIABLE

Definition of a named variable used in an assertion expression.

Attributes

name: String [1..1]

Name of variable.

definition: String [1..1]

Formal definition of the variable.

 
{
    "name": "ASSERTION_VARIABLE",
    "documentation": "Definition of a named variable used in an assertion expression.",
    "properties": {
        "name": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "name",
            "documentation": "Name of variable.",
            "is_mandatory": true,
            "type": "String"
        },
        "definition": {
            "_type": "P_BMM_SINGLE_PROPERTY",
            "name": "definition",
            "documentation": "Formal definition of the variable.",
            "is_mandatory": true,
            "type": "String"
        }
    }
}
aom14.assertion variable

OPERATOR_KIND Enumeration

  • Definition

  • Effective

  • BMM

  • UML

Enumeration

OPERATOR_KIND

Description

Enumeration type for operator types in assertion expressions.

Constants

Signature

Meaning

op_eq

Equals operator (= or ==)

op_ne

Not equals operator (!= or /=)

op_le

Less-than or equals operator (<=)

op_lt

Less-than operator (<=)

op_ge

Greater-than or equals operator (>=)

op_gt

Greater-than operator (>)

op_matches

Matches operator (matches or is_in)

op_not

Not logical operator

op_and

And logical operator

op_or

Or logical operator.

op_xor

Xor logical operator

op_implies

Implies logical operator

op_for_all

For-all (universal) quantifier

op_exists

Exists quantifier

op_plus

Arithmetic plus operator (+)

op_minus

Arithmetic minus operator (-)

op_multiply

Arithmetic multiplication operator (*)

op_divide

Arithmetic division operator (/)

op_exponent

Arithmetic exponentiation operator (^)
OPERATOR_KIND

Enumeration type for operator types in assertion expressions.

Inherits: Any, Ordered, String

Constants

op_eq

Equals operator (= or ==)

op_ne

Not equals operator (!= or /=)

op_le

Less-than or equals operator (<=)

op_lt

Less-than operator (<=)

op_ge

Greater-than or equals operator (>=)

op_gt

Greater-than operator (>)

op_matches

Matches operator (matches or is_in)

op_not

Not logical operator

op_and

And logical operator

op_or

Or logical operator.

op_xor

Xor logical operator

op_implies

Implies logical operator

op_for_all

For-all (universal) quantifier

op_exists

Exists quantifier

op_plus

Arithmetic plus operator (+)

op_minus

Arithmetic minus operator (-)

op_multiply

Arithmetic multiplication operator (*)

op_divide

Arithmetic division operator (/)

op_exponent

Arithmetic exponentiation operator (^)

Functions

is_equal (
other: Any[1]
): Boolean [1..1]

Value equality.
Inherited from Any

infix = (
other: Any[1]
): Boolean [1..1]

Reference equality.
Inherited from Any

instance_of (
a_type: String[1]
): Any [1..1]

Create new instance of a type.
Inherited from Any

type_of (
an_object: Any[1]
): String [1..1]

Type name of an object as a string. May include generic parameters, as in "Interval<Time>".
Inherited from Any

infix < (
other: Ordered[1]
): Boolean [1..1]

Arithmetic comparison. In conjunction with ‘=’, enables the definition of the operators ‘>’, ‘>=’, ‘<=’, ‘<>’. In real type systems, this operator might be defined on another class for comparability.
Inherited from Ordered

infix + (
other: String[1]
): String [1..1]

Concatenation operator - causes ‘other’ to be appended to this string.
Inherited from String

is_empty (): Boolean [1..1]

True if string is empty, i.e. equal to "".
Inherited from String

is_integer (): Boolean [1..1]

True if string can be parsed as an integer.
Inherited from String

as_integer (): Integer [1..1]

Return the integer corresponding to the integer value represented in this string.
Inherited from String

 
{
    "_type": "P_BMM_ENUMERATION_STRING",
    "name": "OPERATOR_KIND",
    "documentation": "Enumeration type for operator types in assertion expressions.",
    "ancestors": [
        "String"
    ],
    "item_names": [
        "op_eq",
        "op_ne",
        "op_le",
        "op_lt",
        "op_ge",
        "op_gt",
        "op_matches",
        "op_not",
        "op_and",
        "op_or",
        "op_xor",
        "op_implies",
        "op_for_all",
        "op_exists",
        "op_plus",
        "op_minus",
        "op_multiply",
        "op_divide",
        "op_exponent"
    ],
    "item_documentations": [
        "Equals operator (= or ==)",
        "Not equals operator (!= or /=)",
        "Less-than or equals operator (<=)",
        "Less-than operator (<=)",
        "Greater-than or equals operator (>=)",
        "Greater-than operator (>)",
        "Matches operator (matches or is_in)",
        "Not logical operator",
        "And logical operator",
        "Or logical operator.",
        "Xor logical operator",
        "Implies logical operator",
        "For-all (universal) quantifier",
        "Exists quantifier",
        "Arithmetic plus operator (+)",
        "Arithmetic minus operator (-)",
        "Arithmetic multiplication operator (*)",
        "Arithmetic division operator (/)",
        "Arithmetic exponentiation operator (^)"
    ]
}
aom14.operator kind