c# – 代码合同：如何表达这些条件？

我现在正在使用Code Contracts,我不完全确定Contract类的静态方法是否足够强大,可以与条件的数学符号竞争.

我们假设我们得到了一个简单的因子方法

int Factorial(int n);

我会表达以下条件：

Precondition:
n >= 0

Postconditions:
Factorial(n) = 1, in case n = 0
Factorial(n) = n*(n-1)*...*1, in case n > 0

这些条件以简洁明了的方式清楚地说明了Factorial的行为.我的问题是,他们是否可以通过代码合同来表达.

前提条件是微不足道的：

Contract.Requires(n >= 0)

条件发布条件可能表示使用

if(n==0)
    Contract.Ensures(Contract.Result<int>() == 1);
if(n > 0)
    ...

但我不喜欢我在这里需要“if”语句的方式,因为它使得前后条件的简单列表更难以阅读.我希望我们会有类似的东西

Contract.Ensures(...).InCase(...);

最后但并非最不重要的是,我不知道如何表达这一点,这是关于数学的常见符号：

n*(n-1)*...*1

猜猜我需要某种循环,但这会复制整个实现.有没有聪明的方式来表达这样的符号？

先感谢您.

解决方法:

您可以尝试以下方法：

Contract.Ensures(Contract.Result<int>() == AlternativeFactorial(n));

AlternativeFactorial在哪里：

[Pure]
public static int AlternativeFactorial(int n)
{
    if(n==0)
        return 1;
    if(n > 0)
    {
        //Alternative implementation.
    }
}

当然,你在合同中使用的任何东西都应该是无副作用的(纯粹的).

现在,就因子实现而言,我无法提出比w0lf更紧凑的“替代”实现.您应该考虑的是将方法的返回值从int更改为BigInteger. Factorials可以非常快地变得非常大.另请注意,通过在factorial值上添加后置条件,您的方法返回结果所需的时间将增加一倍.这可以通过仅在调试配置上构建CodeContracts来解决.

标签：c,specifications,code-contracts
来源： https://codeday.me/bug/20190620/1246828.html