First Order Logic (FOL) to Schematron

Universal quantification

forall(t:x|p(t))

All members of some set x of objects or values shall fulfill predicate p.

every τ(t) in τ(x) satisfies τ(p(τ(t))) where t translates to a unique $ prefixed variable name, and τ(x) translates to current() if the quantification is at the outmost level.

Existential quantification: "at least l and at most h"

exists{l,h}(t:x|p(t))

The number of members of some set x of objects or values, which fulfill predicate p shall be between l and h.

for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return ($var>=τ(l) and $var<=τ(h))

Existential quantification: "exactly n"

exists{n}(t:x|p(t))

The number of members of some set x of objects or values, which fulfill predicate p shall be exactly n.

for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return ($var=n)

Existential quantification: "at most n"

exists{0..n}(t:x|p(t))

The number of members of some set x of objects or values, which fulfill predicate p shall be at most n.

for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return $var<=n)

Existential quantification: "at least n"

exists{n..*}(t:x|p(t))

The number of members of some set x of objects or values, which fulfill predicate p shall be at least n.

for $var in count(for τ(t) in τ(x) return if τ(p(τ(t))) then 1 else ()) return ($var>=n)

Variable access

t defined in a quantification, such as forall(t:x|p(t))

the variable name, either explicitly or implicitly provided

The variable name, preceded by '$' – for example $x1, $c1. NOTE: This is the translation for τ(t), which is mentioned in the Schematron translations of quantifications.

Property call

x.pname

Set of object instances or values reached from the instance or set represented by x by applying property name, pname.

Logical infix

and(x1,...,xn) or(x1,...,xn)

Logical combination as indicated

τ(x1) and ... and τ(xn) τ(x1) or ... or τ(xn)

Negation

not(x)

Logical negation of x

not(τ(x))

Null check

isNull(x)

Determine if the value of x is null.

Equality

isEqualTo(e1,e2)

Equality of expressions e1, e2

τ(e1)= τ(e2)

NOTE: This assumes that equality on sets is fulfilled if at least one pair is equal. Otherwise some more refined code generation will be necessary.

Type check

isTypeOf(x,(ClassLiteral)z)

X is checked for complying with the type y identified by class literal z.

τ(x)[name()='T₁' or … or name()='T_i'], whereT_k is the qualified name of one of the concrete derivations of y, including y, if it is not abstract (names of abstract types are ignored).

String literal

'xxxxx'

same

Numeric literal

123 or 3.1415

same

String literal list

('abc','def',…​)

List of 'names'

same

Class literal

class name (e.g. AirportHeliport)

name of the class

name of the class identified by the class literal