对于可靠的代码，NModel、Spec Explorer、F# 或其他？

Question

我有一个 C# 商业应用程序，带有单元测试。使用 NModel 或 Spec Explorer 可以提高可靠性并减少测试时间和费用吗？或者，如果我用 F#（甚至 Haskell）重写它，我可能会看到什么样的（如果有的话）可靠性提高？

代码合同？阿斯麦？

我意识到这是主观的，并且可能是有争议的，所以如果可能的话，请用数据支持你的答案。 :) 或者也许是一个可行的例子，例如埃里克·埃文斯货运系统？

如果我们考虑

单元测试要具体且强大的定理，已检查 准静态地针对特定的“有趣的实例”和类型为一般但弱的定理（通常静态检查），并契约为一般且强的定理，动态检查在常规程序操作期间发生的特定实例。 （来自 B. Pierce 的被认为有害的类型），

这些在哪里其他工具合适吗？

我们可以使用 Java PathFinder、Scala 等对 Java 提出类似的问题。

Answer 1

可靠性是多个变量的函数，包括软件的总体架构、程序员的能力、需求的质量以及配置管理和一般 QA 流程的成熟度。所有这些都会影响重写的可靠性。

话虽如此，语言确实具有重大影响。在所有其他条件相同的情况下：

• 缺陷大致与 SLOC 数量成正比。更简洁的语言会出现更少的编码错误。 Haskell 似乎需要 C++ 所需 SLOC 的 10% 左右，Erlang 大约 14%，Java 大约 50%。我猜想 C# 在这个规模上可能与 Java 相当。
• 类型系统并不是生来平等的。具有类型推断的语言（例如 Haskell 和较小程度上的 O'Caml）将具有较少的缺陷。 Haskell 特别允许你在类型系统中对不变量进行编码，这样程序只有在它们被证明是正确的情况下才会编译。这样做需要额外的工作，因此请根据具体情况进行权衡。
• 管理状态是许多缺陷的根源。函数式语言，尤其是纯函数式语言，避免了这个问题。
• QuickCheck 及其相关产品允许您编写单元和系统测试来验证一般属性而不是单个测试用例。这可以大大减少测试代码所需的工作，特别是如果您的目标是高测试覆盖率指标。一组 QuickCheck 属性类似于正式规范，并且此概念非常适合测试驱动开发（首先编写测试，当代码通过测试时，您就完成了）。

将所有这些东西放在一起，您应该拥有一个强大的工具包，可以在整个开发生命周期中提高质量。不幸的是，我不知道有任何强有力的研究能够真正证明这一点。我在开始时列出的所有因素都会混淆任何真正的研究，并且在明确的模式显现出来之前您需要大量数据。

Answer 2

在我的“第一”语言 C# 的上下文中，对引用的一些评论：

单元测试要具体且强大
定理，

是的，但它们可能不会给你一阶逻辑检查，比如“对于所有 x 都存在 ay，其中 f(y)”，更像是“存在 ay，这里是 (!), f(y)”，又名设置、行动、断言。 ;)*

准静态检查
特别的“有趣的例子”和
类型为一般但弱的定理
（通常静态检查），

类型不一定那么弱**。

和
合同是通用的和强有力的
定理，动态检查
期间发生的特殊情况
常规程序运行。 （来自 B.
皮尔斯的类型被认为是有害的），

---

单元测试

Pex + Moles 我认为越来越接近一阶逻辑类型的检查，因为它生成边缘情况并使用 C9 求解器来处理整数约束求解。我真的很想看到更多 Moles 教程（moles 用于替换实现），特别是与某种控制反转容器一起使用，该容器可以利用已经存在的抽象类和接口的存根和实际实现。

弱类型

在C#中，它们相当弱，当然：泛型类型/类型允许您为一个操作添加协议语义——即将类型约束在接口上，这是从某种意义上说，实现类同意的协议。然而，协议的静态类型仅适用于一次操作。

示例：反应式扩展 API

让我们以反应式扩展作为讨论主题。

消费者要求的合约，由可观察者执行。

interface IObserver<in T> : IDisposable {
  void OnNext(T);
  void OnCompleted();
  void OnError(System.Exception);
}

该协议还有比该接口显示的更多内容：在 IObserver 上调用的方法<在T>实例必须遵循以下协议：

Ordering:

OnNext{0,n} (OnCompleted | OnError){0, 1}

此外，在另一个轴上； time-dimension:

时间：

for all t|-> t:(method -> time). t(OnNext) < t(OnCompleted)
for all t|-> t:(method -> time). t(OnNext) < t(OnError)

即，在 OnCompleted x 或 OnError 一次之后，不能调用 OnNext。

此外，并行性轴：

并行性：

no invocation to OnNext may be done in parallel

即 IObservable 的实现者需要遵循调度约束。没有 IObservable 可以同时从多个线程推送，而不首先在上下文中同步调用。

您如何以简单的方式测试该合约的持有情况？对于c#，我不知道。

API 的消费者

从应用程序的消费端来看，不同上下文之间可能存在交互，例如调度程序、后台/其他线程，并且最好我们希望保证不会结束陷入僵局。

此外，还需要处理可观察量的确定性处理。扩展方法返回的 IObservable 实例何时处理该方法的参数的 IObservable 实例并处理这些实例可能并不总是很清楚，因此需要了解黑匣子的内部工作原理（或者您可以让引用消失）以“合理的方式”，GC 会在某个时候采取它们）

<<<如果没有 Reactive Extensions，这并不一定更容易：

在 TPL 之上实现了任务池。在任务池中，我们有一个工作窃取委托队列，可以在工作线程上调用。

如果我们改变状态，使用 APM/begin/end 或异步模式（排队到任务池）可能会让我们面临回调排序错误。此外，开始调用及其回调的协议可能过于复杂，因此无法遵循。前几天我读到了一篇关于 silverlight 项目的事后分析，该项目在查看所有回调树的业务逻辑森林时遇到问题。然后就有可能实现穷人的异步 monad，即 IEnumerable，其中异步“管理器”迭代它并在每次生成的 IAsyncResult 完成时调用 MoveNext()。

...并且不要让我开始了解 IAsyncResult 中无数的隐藏协议。

不使用响应式扩展的另一个问题是海龟问题 - 一旦您决定希望 IO 阻塞操作是异步的，就需要有海龟一直到 p/invoke 调用将关联的 Win32 线程放置在 IO 完成端口上！如果您有三层，并且最顶层也有一些逻辑，则需要使所有三层都实现 APM 模式；并履行 IAsyncResult 的众多合同义务（或使其部分损坏）——并且基类库中没有默认的公共 AsyncResult 实现。

>>>>>

使用接口中的异常

即使涵盖了上述内存管理+并行性+契约+协议项，仍然有异常需要以良好、可靠的方式处理（不仅仅是接收和忘记）应用。我想举个例子；

上下文

假设我们发现自己从契约/接口捕获了一个异常（不一定是从反应式扩展的 IObservable 实现中捕获的，它具有单子异常处理而不是基于堆栈帧）。

希望程序员很勤奋并记录了可能的异常，但自始至终都可能存在异常的可能性。如果一切都用代码契约正确定义，至少我们可以确定我们能够捕获一些异常，但是许多不同的原因可能会集中在一个异常类型中，一旦抛出异常，我们如何确保纠正尽可能少的工作？

目标

假设我们正在从应用程序中的消息总线消费者推送一些数据记录，并在后台线程上接收它们，该后台线程决定如何处理它们。

示例

一个现实生活中的例子是 Spotify，我每天都在使用它。

我的 100 美元路由器/接入点有时会认输。我猜它有一个缓存错误或某种堆栈溢出错误，因为每次我通过它推送超过 2 MB/s 的 LAN/WAN 数据时都会发生这种情况。

我必须把网卡注册起来；无线网络和以太网卡。以太网连接断开。 Spotify 事件处理程序循环的套接字返回无效代码（我认为是 C 或 C++）或抛出异常。 Spotify 必须处理它，但它不知道我的网络拓扑是什么样的（并且没有代码来尝试所有路由/更新路由表以及要使用的接口）；我仍然有通往互联网的路线，但只是不在同一个界面上。 Spotify 崩溃了。

论文

例外在语义上根本不够。我相信可以从Haskell中Error monad的角度来看待异常。我们要么继续，要么中断：展开堆栈、执行 catch、执行finally，祈祷我们不会在其他异常处理程序或 GC 上出现竞争条件，或者在未完成的 IO 完成端口上出现异步异常。

但是，当我的某个接口的连接/路由出现故障时，Spotify 就会崩溃并冻结。

现在我们有了 SEH/结构化异常处理，但我认为将来我们将会有 SEH2，其中每个异常源与实际异常一起给出一个可区分的联合（即它应该静态类型化到链接库/程序集），可能的补偿操作 - 在这个示例中，我可以想象 Windows 的网络 API 告诉应用程序执行补偿操作以在另一个接口上打开相同的套接字，或者自行处理它（就像现在一样），或者重试套接字，具有一些内核管理的重试策略。这些选项中的每一个都是可区分联合类型的一部分，因此实现者必须使用其中之一。

我认为，当我们有了 SEH2 时，就不会再被称为例外了。

^^

无论如何，我已经离题太多了。

与其阅读我的想法，不如听听 Erik Meijer 的一些想法 - 这是一个非常好的 他和 Joe Duffy 之间的圆桌讨论。他们讨论了处理调用的副作用。或者查看此搜索列表。

今天，我发现自己处于一个位置，作为一名顾问，维护一个系统，其中更强的静态语义可能会更好，并且我正在寻找可以为我提供编程速度+正确性验证的工具，其级别为准确且精确。我还没找到。

我只是认为，距离面向开发人员的可靠计算，我们还需要 20 年（甚至更多）。现在有太多的语言、框架、营销废话和概念，普通开发人员无法掌握这些知识。

为什么这是在“弱类型”的标题下？

因为我发现类型系统将成为解决方案的一部分；类型不必弱！简洁的代码和强类型系统（比如 Haskell）可以帮助程序员构建可靠的软件。