我正在尝试实现自己的编程语言，目前我正在进行Lexing和解析。我快要完成了，想增加对班级不变性，先决条件和后条件的本机支持。
public withdraw (d64 amount) : this {
require amount > 0;
require this.balance - amount > this.overdraft;
# method code
d64 newBalance = this.balance - amount;
ensure this.balance == newBalance;
}
您还可以在班级顶部定义类不变性。
class BankAccount {
invariant this.balance > this.overdraft;
# class body
}
这些是我的问题：
- 在抽象类或接口中包括类不变性是有意义的。
- 在抽象方法和接口方法中包括前提条件是有意义的。
- 在抽象方法或接口方法中包括后条件是有意义的。
我自己考虑一下，我认为在接口中包括不变性或后条件是没有意义的，但是我真的没有看到先决条件的问题。
可以在下面的抽象和接口方法中包括前和后条件。
public interface BankAccount {
public withdraw (d64 amount) : this {
require amount > 0;
require this.balance - amount > this.overdraft;
# no other statements (implementation)
d64 newBalance = this.balance - amount;
ensure this.balance == newBalance;
}
}
这实际上取决于您的接口是状态还是无状态。在接口方法中包括预/或邮政条件可能是完全可以的。实际上，我们一直这样做。每当您创建一块Javadoc（或任何其他工具）时，都可以创建合同。否则，您如何测试任何东西？重要的是要意识到，测试驱动的开发和逐项合同有很多共同点。定义合同对于适当的TDD至关重要 - 您首先设计界面并为其创建非正式合同（使用人类可读语言）。然后，您编写一个测试以确保满足合同。如果我们遵循TDD古典主义者（https://www.thoughtworks.com/insights/blog/mockists-are-dead-long-long-live-classicists），我们总是对合同进行测试。
现在，要更具体。如果接口是有状态的，我们可以根据其他方法轻松地表达其不变性。让我们以Java List接口为例：
如果您仔细阅读了Javadoc，您会看到很多不变的人。例如，add方法具有以下合同：
-
前提：元素不能为null（如果列表不支持它 - 我认为这是一种设计气味，但让我们放在一边现在）
-
后条件：保留订购，即其他元素无法更改
由于List接口绝对是有状态的，因此我们可以使用查询方法（例如get，sublist等）对列表的状态进行推理，因此，您可以根据接口的方法表达所有不变性。
如果无状态的接口，例如Calculator，我们也定义了合同，但其不变性不包括任何状态。因此，例如，sum方法可以具有以下合同：
int sum(int a, int b)
Preconditions: a and b are integers (which is automatically guaranteed by static type checking in Java)
Postconditions: the result is an integer (again - type safety) which is equal to a + b
我们的 Calculator是一个无状态界面，因此我们不包含任何状态。
现在，让我们回到您的BankAccount示例：
您描述它的方式，BankAccount绝对是一个状态接口。实际上，这是我们称为Entity的模型示例（就域驱动设计而言）。因此，BankAccount具有其生命周期，它的状态可以（并且将在其一生中都可以改变。因此，根据班级的状态方法表达您的合同是完全可以的。您需要做的就是将amount，balance和overdraft移动到接口的顶部，要么作为属性（如果您的语言支持）或方法 - 这并不重要。重要的是，amount，balance和overdraft现在是接口的一部分，并形成接口的无处不在的语言。这些方法/属性是整个BankAccount接口不可或缺的一部分 - 这意味着它们可以用作接口合同的一部分。
前一段时间，我已经实现了一个非常简单的Java合同原型，该原型是由面向方面的编程支持的一组注释。我试图实现与您的类似目标 - 将合同与语言整合在一起并使它们更正式。这只是一个非常简单的原型，但我认为它很好地表达了这个想法。如果您有兴趣 - 我可能应该很快将其上传到GitHub（到目前为止，我一直在使用Bitbucket）。