标签: design-by-contract

我读过编译器可以在编译时强制执行dbc ..它是如何做到的？

前几天我看到了Code Contracts的演示,并决定在一个小测试项目中试一试.

在向类中添加"using System.Diagnostics.Contracts"语句后,我可以适当地设置我的代码合约代码,但似乎没有强制执行合同.

我没有看到项目属性屏幕上出现"代码合同"选项卡的原因吗？

这实际上是一个设计问题.我想知道带有JSON有效负载的Spring3.0 REST Web服务是否提供了类似于遵循契约优先设计的传统Web服务的某种数据协定.我知道JSON的架构类似于XSD,但它在春天适用于哪里？背景:我考虑使用json作为客户端服务器体系结构项目的有效负载,其中客户端是基于.NET的应用程序,数据契约应该提供一种处理客户端的多个版本的方法.客户端应该能够将数据结构发布到服务器.或者我应该采用无模式方法并使用类似于XmlAnyElement的"简单数据绑定"？

作为最佳实践，我们公司使用“合同优先”方法创建Web服务。

在考虑实现之前先定义WSDL。

是否可以通过REST使用这种方法？我当时在考虑使用XSD，但是调用通常不是XML！那么，如何以机器可解释的方式指定合同？

因此,我们正在调查范围保护或类似机制的使用,以确保传入/传出对象的有效性和/或内部状态不变性,类似于C#代码契约.

在正常处理过程中出现意外情况/异常导致某些对象处于不一致状态的特定情况下,我们可以/应该采用什么机制来支持范围守卫将要投诉的事实当我们跳出这个功能？

这里有一些示例伪代码来说明我的观点:

struct IObjectValidator;

struct ObjectValidatorScopeGuard
{
  ObjectValidatorScopeGuard(IObjectValidator * pObj) 
    : m_ptr(pObj) 
  {
    Assert(!m_ptr || m_ptr->isValid());
  }

  ~ObjectValidatorScopeGuard()
  {
    Assert(!m_ptr || m_ptr->isValid());
  }
  private:
    IObjectValidtor * m_ptr;
};


int SomeComponent::CriticalMethod(const ThingA& in, ThingB& inout, ThingC * out)
{
  ObjectValidatorScopeGuard sg1(static_cast<IObjectValidator *>(&in));   
  ObjectValidatorScopeGuard sg2(static_cast<IObjectValidator *>(&inout));
  ObjectValidatorScopeGuard sg3(static_cast<IObjectValidator *>(out));

  // create out
  try
  {
     out = new ThingC();
     out->mergeFrom(inout, out); // (1)
  }
  catch (const EverythingHasGoneHorriblyWrongException& ex)
  {
     // (2) out and inout not guaranteed valid here..
  }
  return 0;
} …

我正在尝试将基本的Design by Contract(由宏实现,它使用内置的assert函数)和Google Test单元测试结合在一个应用程序中.

所以,例如,我有以下代码:

AppFavorite* AppFavorites::Add(const UnicodeString& link)
{
    REQUIRE(!link.IsEmpty());

    ...
}

现在,我无法在单元测试中进行以下测试,因为IDE在到达断言时中止(REQUIRE(!link.IsEmpty());):

TEST(AppFavoritesTest, AddEmpty)
{
    AppFavorites favorites;
    ASSERT_THROW(favorites.Add(L""), std::invalid_argument);
}

那么,我的问题是我应该:

1. 永远不要测试合同所涵盖的条件,或
2. 在单元测试期间以某种方式禁用合同检查？

我无法证明2个循环不变量:

    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre);
    loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m1)[i] == \at(((char*)m2)[i], Pre);

我猜测\对于阵列不起作用,正如我所料.

ACSL by Example(第68页,swap_ranges)中有一个类似的函数,它使用了这个函数,但是如上所述,它们无法用WP插件证明这个特定的函数.我在我的机器上试过它,实际上它无法证明相同的不变量.

完整代码

/*
 * memswap()
 *
 * Swaps the contents of two nonoverlapping memory areas.
 * This really could be done faster...
 */

#include "string.h"

/*@
    requires n >= 1;
    requires \valid(((char*)m1)+(0..n-1));
    requires \valid(((char*)m2)+(0..n-1));
    requires \separated(((char*)m1)+(0..n-1), ((char*)m2)+(0..n-1));
    assigns ((char*)m1)[0..n-1]; …

我一直在想,为什么非C++ OOP语言(不确定是否有其他一些使用标题)没有头文件？

好吧,最让我担心的是,在C++中我可以编写一个类头,然后将它发送给我的伙伴来编译其他代码,而我很乐意按照自己的步调编写类的实际实现.

如何在没有标题的语言中实现这一目标？或许,在我的理解中是否有一些我缺少的东西？

如何与其他同事签订课堂合同,以便两者都可以按照自己的步调进行编码？我应该做一些没有任何方法实现的模拟类,只需要模拟返回,以满足这种需求或如何？

我刚刚添加hibernate-validator-5.1.3.Final.jar到我的类路径并注释了一个POJO:

public class Person {
    @NotNull
    private String name;

    // etc...
}

然后我去用一个驱动程序测试它:

public class Driver {
    public static void main(String[] args) {
        Person p = new Person();
        p.setName(null);
    }
}

执行时不会抛出任何验证错误 - 我哪里出错了？

有没有办法为前置和后置条件指定自定义错误/失败消息，类似于Predicate_Failurefor 谓词？我似乎无法在官方文档中找到任何内容。TIA。

处理以下情况的首选方法是什么:

switch (numberOfActualBytes)
{
    case 1: return something1;
    case 2: return something2;
    case 3: return something3;
    case 4: return something4;
}

我肯定知道numberOfActualBytes由于使用过的合同是在范围内1-4.

我该如何编写不会导致not all code paths return a value错误的代码？

我怀疑我应该在这个函数结束时抛出一些异常default switch case,但是可能有一个更好的解决方案.