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.