标签: design-by-contract

据我所知,在DbC方法中,前置条件和后置条件附加到函数中.

我想知道的是,这是否也适用于成员函数.

例如,假设我在每个公共函数末尾的开头使用不变量,成员函数将如下所示:

编辑:(清理我的例子)

void Charcoal::LightOnFire() {
  invariant();
  in_LightOnFire();

  StartBurning();    
  m_Status = STATUS_BURNING;
  m_Color = 0xCCCCCC;

  return; // last return in body

  out_LightOnFire();
  invariant();
}

inline void Charcoal::in_LightOnFire() {
  #ifndef _RELEASE_
  assert (m_Status == STATUS_UNLIT);
  assert (m_OnTheGrill == true);
  assert (m_DousedInLighterFluid == true);
  #endif
}

inline void Charcoal::out_LightOnFire() {
  #ifndef _RELEASE_
  assert(m_Status == STATUS_BURNING);
  assert(m_Color == 0xCCCCCC);
  #endif
}

// class invariant
inline void Charcoal::invariant() {
  assert(m_Status == STATUS_UNLIT || m_Status == STATUS_BURNING || m_Status == STATUS_ASHY);
  assert(m_Color == 0x000000 …

我正在阅读有关 dbc 的内容（http://en.wikipedia.org/wiki/Design_by_contract）有人能给我一个使用与继承相关的类不变量的简单示例吗？

我没有看到很多开发人员使用Java Assert,但我非常热衷于使用它们.你能分享一些有效使用它们的技巧吗？

我想通过合同跳进编码.我得到了VS2010(使用C#4.0编译器),但我必须针对3.5框架.

合同库的第三方代码是什么类和接口最像.NET 4.0的类？

请告诉我这些功能的作用.

我正在学习先决条件以及何时使用它们。有人告诉我，前提条件是

@pre fileName must be the name of a valid file

不适合以下代码：

/**
Creates a new FileReader, given the name of file to read from.
@param fileName- the name of file to read from
@throw FileNotFoundException - if the named file does not exist,
is a directory rather than a regular file, or for some other reason cannot
be opened for reading.
*/
public FileReader readFile(String fileName) throws FileNotFoundException {
. . .
}//readFile

为什么是这样？

编辑：另一个例子

作为示例，我们假设以下内容是以“正确”的方式完成的。请注意 IllegalArgumentException 和前提条件。请注意如何明确定义行为，以及如何在设置前提条件的情况下进行 throws …

看来,NotNull和ContractAnnotation("key: null => halt")在其上的R·效果相当类似.有什么东西我错过了吗？我应该经常同时申请吗？

在调用初始化列表之前是否可以断言类构造函数上的参数？

class Foo
{
    int m_lower;
    int m_upper;
    unsigned int m_delta;

  public:
    Foo(int t_lower, int t_upper) :
        assert(t_lower < t_upper),  // Assert here, before initialisation of fields.
        m_lower(t_lower),
        m_upper(t_upper),
        m_delta(t_upper - t_lower)
    {
       // Assert could be made here, but m_delta would have underflowed if t_upper < t_lower.  
    }
}

在初始化列表之前断言的好处是可以立即提出每个字段的初始化要求，并且不必对具有相同要求的每个初始化进行多次检查。虽然 m_delta 的初始化可以在初始化方法中进行init_delta，但如果多个值具有相同的要求，t_upper > t_lower则必须将断言放置在每个值中（以防先前的断言被删除）。如果放置在构造函数本身中，则一个或多个字段的初始化可能已经失败（出现比下溢更戏剧性的情况）。

如果放置在初始化列表的顶部，则合约在检查时对用户来说是清楚的，并且会在发生任何错误（例如本例中的下溢）之前标记错误。

上述案例只是该问题的一个简化示例。我知道有更好的方法来解决上述特定问题（abs() 等）。

感谢您的帮助和建议！

我最近一直在看DbC和Spec#似乎支持非可空对象.不幸的是,Spec#似乎已被抛弃.

1. Spec#似乎内置了许多不错的语言功能,为什么它被抛弃了？
2. 默认情况下让所有对象都不可为空可能有任何问题所以你必须写int？,string？甚至MailMessage？如果你真的想要一个可以为空的对象？
3. 我在这里看到类似的Sql类比,你可以将类属性检查为可空或不可空.您是否可以使用sql表列对属性进行约束？

我没有看到在语言中内置这样的功能的问题.有人能开导我吗？

我是IntelliJ的新手.尝试使用cofoja代码注释时,我在构建时会收到以下错误.

Error:java: error in contract: package com.google.java.contract.core.agent does not exist
Error:java: error in contract: package com.google.java.contract does not exist

我的项目是针对Oracle JDK 1.7.我正在使用io.konverge发布的cofoja版本和IntelliJ 14.1.4.

<dependency>
  <groupId>io.konverge</groupId>
  <artifactId>cofoja</artifactId>
  <version>2.0.0</version>
</dependency>

从maven命令行构建项目时,我没有收到遇到的错误.

编辑:

这是一个使用maven编译好的cofoja项目示例,但我无法在IntelliJ中构建.

https://github.com/konvergeio/cofoja-example

我cofoja在GitHub上的项目票证中附加了此项目的IntelliJ DEBUG构建日志:https://github.com/nhatminhle/cofoja/issues/45

编辑2:

更新了特定于cofoja-example项目的问题.