esverify
esverify copied to clipboard
Support for subclasses and inheritance
The current rudamentary support for (immutable) classes does not include inheritance. However, it should be possible to extend a superclass, use super and check whether the overriden methods adhere to subtyping laws (co/contravariance).
Example:
class A {
f(n) {
requires(n >= 0);
ensures(result => typeof result === 'number');
return 23;
}
}
class B extends A {
f(n) { // Overridden method can have a
requires(typeof n === 'number'); // broader precondition and a
ensures(result => result >= 0); // more precise postcondition.
return 23;
}
}