多态类
多态类可以用来系统地引入表示代数的符号系统。
例如,让我们从库类的草图开始 Eq 它引入了等价关系:
class Eq[t] {
virtual fun == : t * t -> bool;
virtual fun != (x:t,y:t):bool => not (x == y);
axiom reflex(x:t): x == x;
axiom sym(x:t, y:t): (x == y) == (y == x);
axiom trans(x:t, y:t, z:t): x == y and y == z implies x == z;
fun eq(x:t, y:t)=> x == y;
fun ne(x:t, y:t)=> x != y;
}
类只有一个类型参数 t . 二 virtual 首先介绍功能, == 等效性,以及 != 因为不相等。
类型 == 函数已给定,但未定义。我们只有接口。
不等价性被定义为等价性的否定。
接下来,我们有三个公理来指定所需的语义。
第一条公理, reflexivity ,表示值等于自身。
第二条公理, symmetry ,表示a如果x等于y,那么y等于x。
第三条公理, transitivity 如果x等于y,y等于z,那么z也等于z。
在这种情况下,这三条定律是一个完整的规范,而且,这三条定律是独立的,因为一条定律不能从另一条定律中推导出来。这两个性质意味着我们的规则实际上是数学公理。
Felix不要求 axioms 实际上是公理。然而,可以从所述公理导出的简单规则可以通过 lemma . 它的思想是引理可以从公理中被很容易地证明,以至于一个自动的定理证明者可以做到这一点,而不需要任何进一步的帮助。
你也可以 theorem 这是一个可以从公理中证明的规则,但是如果证明需要一个人,或者一个有证明助手的人来证明它的正确性。
最后,在我们的类中,我们有两个用虚函数定义的命名函数。注意这些函数不是虚函数。