Hallo everyone, I came across the the following questions regarding RM invariants since there’s an upcoming new version, also about Interval class.
Use of generating_type: in both RM there’s use for function generating_type in multiple invariants & post condition. For example in class Entry, invariant Subject_validity: subject_is_self implies subject.generating_type = “PARTY_SELF”, this function declaration doesn’t seem to be found anywhere, is it a declared builtin function. how does it differ from using {Any}.instance_of(subject) Which is already declared in class Any.
Interval invariants: the class Interval<T> invariants doesn’t hold for intervals where both lower and upper are included and bounded except when T: DV_ORDERED, invariant fails because it attempts to look up the strictly_comparable_to method directly on the target object. Since other types like Integer is a primitive that does not inherit from DV_ORDERED, this specific method is never explicitly declared inside it. Consequently, evaluating the expression for [0,1] triggers a semantic type error for a missing method rather than successfully returning true. So since DV_INTERVAL, already adds this invariant below wouldn’t be better to be removed from Interval<T>?
This is just an accessor that obtains the type name.
Yes, this was a bad idea from the first place. Such semantic correctness can only be tested from some interface like this one, with extra functions added to test comparability. Anyway it shouldn’t be in the data types.
I understood it as function that obtains the dynamic type of the instance rather than the static, but when I looked into the amendment record in release 1.0, it appears that it was part of class Any explicitly. but now from what I understand it seems to be replaced with {Any}.type_of(obj): String (sorry I was wrong in the before, not instance_of). I looked in both RM and Base, and generating_type is not explicitly specified anywhere.
Amendment record:
R E L E A S E 1.0 : CR-000188: Add generating_type function to ANY for use in invariants. ,T Beale , 2006
If I may ask, wouldn’t it be sufficient removing just that specific invariant?
since the invariant Limits_consistent: (not upper_unbounded and not lower_unbounded) implies lower <= upper already holds for primitive types (Double, Integer, Real, Integer64), because they are a leaf types and dynamically there’s nothing below them so if you have Interval<Double> both lower and upper are definitely comparable because there’s no descendant class that changes the logic of their comparability.
because,In DV_INTERVAL there’s already the invariant that forces strictly_comparable_to because it takes DV_ORDERED so that invariant is logical there.
I tried to trace back the origins of generating_type:
After checking the old pdf document of release 1.0, it seems that the amendment record mentions the addition of generating_type to Any, but in class description itself specifies property called type rather that generating type, which has same logical function (getting dynamic type). Its use:generating_type sill wasn’t used in RM classes invariants here.
in release 1.01, neither type nor generating_type are in class Any. Its use: in this release, generating_type was incorporated to RM classes invariants.
in release 1.02, the function type_of(obj) was added to Any, but no description.
Description of type_of(obj) wasn’t added until release 1.0.4, after it was moved to BASE.
Knowing this, should it be considered an issue or a bug? or is it considered as part of the builtin syntax?
or should it be replaced with {Any}.type_of(obj) ?
Hi,
It could be a documentation bug - some leftover, either was not removed when it supposed to be, or wasn’t consistently added when it supposed to be. Personally, I don’t quite understand the need of this function in particular, in the programming languages that I am using nowadays. Can you be more precise on what do you suggest and why would that be necessary or good to do; perhaps make a SPECPR Jira ticket so that we can track it properly.
Interval: dropping the invariant that is using strictly_comparable_to since it is logically wrong, since T can be types other than DV_ORDERED.It can be left to the type property type itself for Interval<T>. for example if it is Integer, that by itself would allow both lower&upper, since these Ordered are primitive and are leaflet types and they don’t have child classes(Integer, Double, Real …etc).
generating_type: two solutions come to mind:
replacing all its uses with {Any}.type_of since it is already specified in Any.
adding generating_type to Any and dropping Any::type_of(obj).
Note: I think first option is better because it gives implementers more freedom how to store the dyanmic type. or maybe make generating_type as an argumentless function inside Anyand remove the need.
Reasoning:
for Interval: it is semantically incorrect to use a function of child class inside the the parent. because this would cause the
for generating_type: abiding by more specified function inside the Spec.
Importance for both: semantical correctness for the use expression. for example: if implmentation is parsing invariants, pre & postconditions as BEL or EL, and running interpreter to execute these invariants instead hardcoding them in the host programming language. So using generating_type results an error , that this property is not availabe. Similar thing for Interval<Integer> wouldn’t hold because Integer doens’t have strictly_comparable_to.
The reason I didn’t open an issue is that I don’t know the future trajectory of OpenEHR after pausing BMMv3, it seemed previously that it would be using EL as unviseral language for the whole spec(invariants post&preconditions, ADL). So I opened it for discussion rather than considering it a bug directly and wasting time & resources on it, if it is considered harmless based on future plans.
My Use case as an example:
I thought since EL would be universal language in the spec and based on BMM, why not create a simple interpter that runs EL as language directly(fit for BEL too which is currently used inside ADL) that can run these expressions and statement directly.
Therefore, the current flow is: I allocate memory for the instance=>the deserializer fills that buffer=>the Interpreter executes the invariants to ensure the instance is abiding by the contract.
This makes the implementation more stable for changes in the spec ( if an invariant changed for example or a new class is introduced) and makes it more uniform - same interpter for ADL and invariants -, but at the same it requires semantical, logical and syntactical correctness.
I think I agree with both solution you proposed - it makes sense, as much as I understand it now (but I might not oversee yet all impact).
About BMMv3 I don’t know when and if that would be continued; we need somebody to work on it, and community/vendors to adopt it - there should be a demand for it. But we can fix the specs at the point you mentioend anyways.
same here, regarding the fix ofInterval invariant is simple, but for generating_type it depends on which solution. refactoring all the expressions that because it is used alot in RM and I think that I saw it in AM2(in a pseudocode), on the other side if it is added to Any instead of type_of(preferably as argumentless function to hide underlying implementation of ) doesn’t need refactoring - since also till now I don’t remember being used.
it definitely makes sense, since invariants, pre- and post-conditions rely on fundamental syntax like boolean logic, property access, and function calls, keeping them semantically sound gives openehr a reliable base to build on—whether for future BMMv3 work(hopefully) or external extensions like SPLASH.
With that in mind, do you think it would be better that I open issue when I spot similar bugs in the specification going forward?
Yes it is definitely a good idea; the worst can happen (in general) is that ticket is rejected (or deferred or delayed - to be honest thats even worse) - but your report and analysis looks pretty sound, and the fix might be easygoing to be picked up soon.
Thank you again for your work on this.