继承

定义类时,可以从其他类或其专门化继承方法。例如这里有一个 total order

class Tord[t]{
  inherit Eq[t];

  virtual fun < : t * t -> bool;
  fun lt (x:t,y:t): bool=> x < y;

  axiom trans(x:t, y:t, z:t): x < y and y < z implies x < z;
  axiom antisym(x:t, y:t): x < y or y < x or x == y;
  axiom reflex(x:t, y:t): x < y and y <= x implies x == y;
  axiom totality(x:t, y:t): x <= y or y <= x;

  fun >(x:t,y:t):bool => y < x;
  fun gt(x:t,y:t):bool => y < x;

  fun <= (x:t,y:t):bool => not (y < x);
  fun le (x:t,y:t):bool => not (y < x);

  fun >= (x:t,y:t):bool => not (x < y);
  fun ge (x:t,y:t):bool => not (x < y);

  fun max(x:t,y:t):t=> if x < y then y else x endif;
  fun \vee(x:t,y:t) => max (x,y);

  fun min(x:t,y:t):t => if x < y then x else y endif;
  fun \wedge(x:t,y:t):t => min (x,y);
}

这个 inherit 语句引入了情商的方法,因此您可以写下:

println$ Tord[int]::eq(1,2);

希望它能起作用。但是,当实例化一个总订单时 不能 提供继承方法的定义,则必须提供原始类的实例:

instance Eq[int] {
  fun == : int * int -> bool = "$1==$2";
}
instance Tord[int] {
  fun < : int * int -> bool = "$1<$2";
}

虽然在这种情况下,我们继承了情商 [t] 尽管如此,我们还是可以继承情商 [int] 例如。只能为类提供实例,而不能为专门化提供实例,因为实例本身就是定义专门化的。