behavioural-subtyping:OOP 行为子类型检查器

行为子类型检查器 ＃＃概述 Checker 是作为安特卫普大学的概念验证而开发的。 检查一个类是否是另一个类的行为子类型，即符合 Liskov 替换原则，比较所有覆盖字段和方法的契约，并确保它们不会强加比它们的超类相等的更多限制条件。 虽然有多种工具可在运行时提供此功能，但尚未开发出一种静态服务于同一目的的工具。 这篇文章深入探讨了这种可能性。 合同由开发人员以形式逻辑编写为 Java 注释。 然后将它们组合成更复杂的公式，并提供给 Microsoft Research 的 。 支持两种注释： **Requires**: Preconditions for methods. **Invariant**: Constraints that must be preserved inside a code block. ＃＃用法 合同必须以格式编写。 由于这是 LSP 静态验证概念的证