契约式设计框架

Kevin McFarlane

4.95/5 (32投票s)

2002年2月21日

6分钟阅读

322003

1516

一个实现契约式设计的 C# 库。

下载源文件 - 5Kb

此类库提供了一个契约式设计框架，供 .NET 项目使用。下载中还包含一个 Visual Basic .NET 版本，但以下讨论以 C# 为准。在这两种情况下，任何 .NET 语言编写的 .NET 客户端都可以使用该库。（尽管如果使用 VB.NET 版本，则 IntelliSense 代码注释在客户端应用程序中将不可见。）

“契约式设计”是由 Bertrand Meyer 在 Eiffel 编程语言中推广的一种方法，该语言将支持内置于语言结构中。

请参阅 Bertrand Meyer 的《面向对象软件构造》（面向对象软件构造）- 第二版（Prentice Hall, 1997）第 11 章，以及《构建无 Bug 的面向对象软件：契约式设计入门》。

基本思想是，一个类可以被视为与其客户端之间存在契约，其中该类保证提供某些结果（其方法的后置条件），前提是客户端同意满足某些要求（类方法的先决条件）。例如，考虑一个例程

string FindCustomer(int customerID)

先决条件可能是 `customerID` 为正。后置条件可能是我们保证找到该客户，即，可能在其他事情中，返回值是一个非空字符串。

先决条件失败表明调用者（客户端）存在 bug。后置条件失败表明例程（供应商）存在 bug。这些条件或规范是通过断言语句实现的。在 C/C++ 代码中，`assert` 宏用于这些目的。.NET Framework 类库使用 `System.Diagnostics` 命名空间中可用的断言函数。默认情况下，这些函数在断言失败时会生成“中止、忽略、重试”消息框。另一种方法是使用异常处理。这是我下面描述的框架所采用的方法，尽管我也将 .NET 断言函数包装起来作为一种替代方案。

在 C# 中，我们无法像 Eiffel 那样全面，但我们可以走一小段路。该库提供了一组静态方法，用于定义先决条件、后置条件、类不变量和一般断言以及表示它们的异常类。还提供了调用 .NET ` System.Diagnostics.Trace()` 断言的方法，以替代抛出异常。调试时，有时您希望能够忽略断言并继续逐行执行代码，尤其是在例程仍处于变化状态时。例如，一个断言可能不再有效，但您仍然希望标记该断言，以提醒您必须修复代码（删除断言或将其替换为另一个）。

将代码构建成 C# 库后，您可以将其引用包含在任何 .NET 语言编写的 .NET 客户端应用程序中。然后，您只需要导入 `DesignByContract` 命名空间。

对于导入 `DesignByContract` 命名空间的每个项目，您可以

生成调试断言而不是异常。
单独启用或禁用先决条件、后置条件、不变量和断言检查。
为每个断言提供描述，或不提供。如果您不提供，框架将告诉您生成的是什么类型的错误 - 先决条件、后置条件等。
为 Debug 和 Release 构建定义不同的规则。

契约与继承

在将契约式设计用于继承时，应遵守某些规则。Eiffel 具有强制执行这些规则的语言支持，但在 C# 中，我们必须依赖程序员。规则是，在派生类中（Meyer，第 16 章）

重写的方法可以 [仅] 削弱先决条件。这意味着派生类中的先决条件应与被覆盖的先决条件进行逻辑“或”运算。
重写的方法可以 [仅] 加强后置条件。这意味着派生类中的后置条件应与被覆盖的后置条件进行逻辑“与”运算。
派生类的类不变量应与其基类的类不变量进行逻辑“与”运算。

示例（使用伪 C# 语法）

class D inherits B

public virtual int B.Foo(int x)
{
  Check.Require(1 < x < 3);
  ...
  Check.Ensure(result < 15);
  return result;
}

public override int D.Foo(int x)
{
  Check.Require (1 < x < 3 or 0 < x < 5); // weakened precondition
  ...
  Check.Ensure (result < 15 and result < 3); // strengthened postcondition
  return result;
}

Eiffel 具有支持上述内容的语言结构。在 `D.Foo()` 中，我们将编写

require else 0 < x < 5

意思是“首先检查基类先决条件，如果失败，则检查派生类版本。”

ensure then result < 3

意思是“检查基类后置条件和派生类后置条件，并确保它们都通过。”

对于 C#，我们只需编写

Check.Require(0 < x < 5 )
Check.Ensure(result < 3)

确保先决条件始终等于或弱于基类版本，后置条件始终等于或强于基类版本。

对于不变量，在 B 中我们可能有

Check.Invariant(B.a > 0 and B.b > 0);

而在 D 中

Check.Invariant(D.c > 0 and D.d > 0);

规则说我们应该在 D 中组合这些

Check.Invariant(B.a > 0 and B.b > 0 and D.c > 0 and D.d > 0);

或

Check.Invariant(B.a > 0 and B.b > 0);
Check.Invariant(D.c > 0 and D.d > 0);

条件编译常量

用于启用和禁用每种类型的契约。

这些建议基于 Meyer p393。

`DBC_CHECK_ALL` - 检查断言 - 暗示检查先决条件、后置条件和不变量。
`DBC_CHECK_INVARIANT` - 检查不变量 - 暗示检查先决条件和后置条件。
`DBC_CHECK_POSTCONDITION` - 检查后置条件 - 暗示检查先决条件。
`DBC_CHECK_PRECONDITION` - 仅检查先决条件，例如，在 Release 版本中。

因此，要启用所有检查，请写入

#define DBC_CHECK_ALL // at the top of the file

或者，作为全局设置，可以在项目属性对话框中定义条件编译常量。您可以为 Release 版本指定与 Debug 版本不同的常量。推荐的默认设置是

Debug 版本中的 `DBC_CHECK_ALL`
Release 版本中的 `DBC_CHECK_PRECONDITION`

后者意味着只有您的代码中的 `Check.Require` 语句将被执行。`Check.Assert`、`Check.Ensure` 和 `Check.Invariant` 语句将被忽略。此行为是通过放置在 `Check` 类下方每个方法之前的条件属性实现的。

例如，方法上方的 `[Conditional("DBC_CHECK_ALL")`、`Conditional("DBC_CHECK_INVARIANT")]` 意味着只有在定义了 `DBC_CHECK_ALL` 或 `DBC_CHECK_INVARIANT` 时才会执行该方法。

示例

C# 客户端

using DesignByContract;
...
public void Test(int x)
{
  try
  {
    Check.Require(x > 0, "x must be positive.");
  }
  catch (System.Exception ex)
  {
    Console.WriteLine(ex.ToString());
  }
}

您可能还希望合并 .NET Framework 自己的异常（例如，用于无效参数等）。在这种情况下，catch 块应该更细化。例如，

using DesignByContract;
...
public void Test(int x)
{
  try
  {
    Check.Require(x > 0, "x must be positive.", 
                      new ArgumentException("Invalid argument.", "x"));
  }
  catch (DesignByContractException ex)
  {
    Console.WriteLine(ex.GetType().ToString() + "\n\n" 
                      + ex.Message + "\n\n" + ex.StackTrace);
    Console.WriteLine("Retrieving exception history...");

    Exception inner = ex.InnerException;

    while (inner != null)
    {
      Console.WriteLine(inner.GetType().ToString() + "\n\n"
                           + inner.Message + "\n\n" + inner.StackTrace);
      inner = inner.InnerException;
    }
  }
  catch (Exception ex)
  {
    Console.WriteLine(ex.GetType().ToString() + "\n\n"
                                 + ex.Message + "\n\n" + ex.StackTrace);
  }
}

如果您希望使用用于调试场景的跟踪断言语句，而不是异常处理，请设置

Check.UseAssertions = true;

您可以在应用程序的入口点指定此设置，并可能使其依赖于条件编译标志或配置文件设置，例如：

#if DBC_USE_ASSERTIONS
Check.UseAssertions = true;
#endif

您可以将输出重定向到 Trace 侦听器。例如，您可以插入

Trace.Listeners.Clear();
Trace.Listeners.Add(new TextWriterTraceListener(Console.Out));

或将输出重定向到文件或事件日志。

VB 客户端

Imports DesignByContract
...
Sub Test(ByVal x As Integer)
  Try
    Check.Require(x > 0, "x must be positive.")
  Catch ex As System.Exception
    Console.WriteLine(ex.ToString())
  End Try
End Sub

限制

目前，该库不能用于需要远程的异常。要实现这一点，每个异常类都必须标记为 `[Serializable]`，并且还必须提供反序列化构造函数，如 Eric Gunnerson（Microsoft Corporation）在文章 《The Well-Tempered Exception》 中所述。

框架

注意：为了在客户端应用程序中查看 IntelliSense 代码注释，您需要编辑类库的“项目属性”->“配置属性”设置。在“输出”->“XML 文档”部分，输入：`bin\Debug\DesignByContract.xml`。路径是您的 DLL 的路径。另外，请确保 DLL 和 .xml 文件名共享相同的名称前缀，即，如果库名为 `DesignByContract`，则文档文件名应为 `DesignByContract.xml`。

  public sealed class Check
  {
    #region Interface

    /// <summary>
    /// Precondition check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void Require(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PreconditionException(message);
      }
      else
      {
        Trace.Assert(assertion, "Precondition: " + message);
      }
    }

    /// <summary>
    /// Precondition check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void Require(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PreconditionException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Precondition: " + message);
      }
    }

    /// <summary>
    /// Precondition check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void Require(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PreconditionException("Precondition failed.");
      }
      else
      {
        Trace.Assert(assertion, "Precondition failed.");
      }
    }

    /// <summary>
    /// Postcondition check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void Ensure(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PostconditionException(message);
      }
      else
      {
        Trace.Assert(assertion, "Postcondition: " + message);
      }
    }

    /// <summary>
    /// Postcondition check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void Ensure(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PostconditionException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Postcondition: " + message);
      }
    }

    /// <summary>
    /// Postcondition check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void Ensure(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new PostconditionException("Postcondition failed.");
      }
      else
      {
        Trace.Assert(assertion, "Postcondition failed.");
      }
    }

    /// <summary>
    /// Invariant check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void Invariant(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new InvariantException(message);
      }
      else
      {
        Trace.Assert(assertion, "Invariant: " + message);
      }
    }

    /// <summary>
    /// Invariant check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void Invariant(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new InvariantException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Invariant: " + message);
      }
    }

    /// <summary>
    /// Invariant check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void Invariant(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new InvariantException("Invariant failed.");
      }
      else
      {
        Trace.Assert(assertion, "Invariant failed.");
      }
    }

    /// <summary>
    /// Assertion check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL")]
    public static void Assert(bool assertion, string message)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new AssertionException(message);
      }
      else
      {
        Trace.Assert(assertion, "Assertion: " + message);
        //Trace.Assert(assertion, "Assertion: " + message);
      }
    }

    /// <summary>
    /// Assertion check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL")]
    public static void Assert(bool assertion, string message, Exception inner)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new AssertionException(message, inner);
      }
      else
      {
        Trace.Assert(assertion, "Assertion: " + message);
      }
    }

    /// <summary>
    /// Assertion check.
    /// </summary>
    [Conditional("DBC_CHECK_ALL")]
    public static void Assert(bool assertion)
    {
      if (UseExceptions)
      {
        if (!assertion) throw new AssertionException("Assertion failed.");
      }
      else
      {
        Trace.Assert(assertion, "Assertion failed.");
      }
    }

    /// <summary>
    /// Set this if you wish to use Trace Assert statements
    /// instead of exception handling.
    /// (The Check class uses exception handling by default.)
    /// </summary>
    public static bool UseAssertions
    {
      get
      {
        return useAssertions;
      }
      set
      {
        useAssertions = value;
      }
    }

    #endregion // Interface

    #region Implementation

    // No creation
    private Check() {}

    /// <summary>
    /// Is exception handling being used?
    /// </summary>
    private static bool UseExceptions
    {
      get
      {
        return !useAssertions;
      }
    }

    // Are trace assertion statements being used?
    // Default is to use exception handling.
    private static bool useAssertions = false;

    #endregion // Implementation

    #region Obsolete

    /// <summary>
    /// Precondition check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Require")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void RequireTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Precondition: " + message);
    }


    /// <summary>
    /// Precondition check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Require")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION"),
    Conditional("DBC_CHECK_PRECONDITION")]
    public static void RequireTrace(bool assertion)
    {
      Trace.Assert(assertion, "Precondition failed.");
    }

    /// <summary>
    /// Postcondition check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Ensure")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void EnsureTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Postcondition: " + message);
    }

    /// <summary>
    /// Postcondition check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Ensure")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT"),
    Conditional("DBC_CHECK_POSTCONDITION")]
    public static void EnsureTrace(bool assertion)
    {
      Trace.Assert(assertion, "Postcondition failed.");
    }

    /// <summary>
    /// Invariant check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Invariant")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void InvariantTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Invariant: " + message);
    }

    /// <summary>
    /// Invariant check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Invariant")]
    [Conditional("DBC_CHECK_ALL"),
    Conditional("DBC_CHECK_INVARIANT")]
    public static void InvariantTrace(bool assertion)
    {
      Trace.Assert(assertion, "Invariant failed.");
    }

    /// <summary>
    /// Assertion check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Assert")]
    [Conditional("DBC_CHECK_ALL")]
    public static void AssertTrace(bool assertion, string message)
    {
      Trace.Assert(assertion, "Assertion: " + message);
    }

    /// <summary>
    /// Assertion check.
    /// </summary>
    [Obsolete("Set Check.UseAssertions = true and then call Check.Assert")]
    [Conditional("DBC_CHECK_ALL")]
    public static void AssertTrace(bool assertion)
    {
      Trace.Assert(assertion, "Assertion failed.");
    }
    #endregion // Obsolete

  } // End Check

  #region Exceptions

  /// <summary>
  /// Exception raised when a contract is broken.
  /// Catch this exception type if you wish to differentiate between
  /// any DesignByContract exception and other runtime exceptions.
  ///
  /// </summary>
  public class DesignByContractException : ApplicationException
  {
    protected DesignByContractException() {}
    protected DesignByContractException(string message) : base(message) {}
    protected DesignByContractException(string message, Exception inner) : 
                                                   base(message, inner) {}
  }

  /// <summary>
  /// Exception raised when a precondition fails.
  /// </summary>
  public class PreconditionException : DesignByContractException
  {
    /// <summary>
    /// Precondition Exception.
    /// </summary>
    public PreconditionException() {}
    /// <summary>
    /// Precondition Exception.
    /// </summary>
    public PreconditionException(string message) : base(message) {}
    /// <summary>
    /// Precondition Exception.
    /// </summary>
    public PreconditionException(string message, Exception inner) : 
                                            base(message, inner) {}
  }

  /// <summary>
  /// Exception raised when a postcondition fails.
  /// </summary>
  public class PostconditionException : DesignByContractException
  {
    /// <summary>
    /// Postcondition Exception.
    /// </summary>
    public PostconditionException() {}
    /// <summary>
    /// Postcondition Exception.
    /// </summary>
    public PostconditionException(string message) : base(message) {}
    /// <summary>
    /// Postcondition Exception.
    /// </summary>
    public PostconditionException(string message, Exception inner) : 
                                              base(message, inner) {}
  }

  /// <summary>
  /// Exception raised when an invariant fails.
  /// </summary>
  public class InvariantException : DesignByContractException
  {
    /// <summary>
    /// Invariant Exception.
    /// </summary>
    public InvariantException() {}
    /// <summary>
    /// Invariant Exception.
    /// </summary>
    public InvariantException(string message) : base(message) {}
    /// <summary>
    /// Invariant Exception.
    /// </summary>
    public InvariantException(string message, Exception inner) : 
                                           base(message, inner) {}
  }

  /// <summary>
  /// Exception raised when an assertion fails.
  /// </summary>
  public class AssertionException : DesignByContractException
  {
    /// <summary>
    /// Assertion Exception.
    /// </summary>
    public AssertionException() {}
    /// <summary>
    /// Assertion Exception.
    /// </summary>
    public AssertionException(string message) : base(message) {}
    /// <summary>
    /// Assertion Exception.
    /// </summary>
    public AssertionException(string message, Exception inner) : 
                                            base(message, inner) {}
  }

  #endregion // Exception classes

} // End Design By Contract