esverify icon indicating copy to clipboard operation
esverify copied to clipboard

Support for subclasses and inheritance

Open levjj opened this issue 6 years ago • 0 comments

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;
  }
}

levjj avatar Jul 20 '19 22:07 levjj