合同“true”，使得“assert true x==x”成立答案

【问题标题】：Contract "true", such that "assert true x==x" holds合同“true”，使得“assert true x==x”成立
【发布时间】：2019-09-15 09:25:26
【问题描述】：

是否可以编写一份合同来检查一个陈述是否正确？比如我要定义一个合约

true :: Contract a

使得对于所有值 x，等式

assert true x == x

持有。

我尝试过这样的事情：

true :: Contract a
true = Pred (\a -> True)

但是当运行assert true x == x 编译器说x 是未定义的。运行assert true 5==6 时，结果是False，我希望得到Contract violation error。我应该如何更改这个true 合同？非常感谢您的帮助。

这里

data Contract :: * -> * where
  Pred :: (a -> Bool) -> Contract a
  Fun  :: Contract a -> Contract b -> Contract (a -> b)

Assert 违反合约会导致运行时失败，否则返回原始结果：

assert :: Contract a -> a -> a
assert (Pred p)       x = if p x then x else error "contract violation"
assert (Fun pre post) f = assert post . f . assert pre

【问题讨论】：

我假设这是使用库。你能指定你使用的是哪个库吗？
@bradrn 我没有。我自己定义了合同类型和断言函数
那你能给我们提供定义吗？除非我们知道您在使用什么，否则我们无法帮助您。
@bradrn 我做到了。在“这里”这个词之后，在问题的结尾。（我编辑了问题）
旁注：Haskell 有很多表达式，但语句不多（报告将import 和do 中的条目描述为语句）。

标签： haskell contract

【解决方案1】：

如果您考虑您对true 和assert 的定义，您可以非常清楚地看到问题所在。以下是相关部分：

true :: Contract a
true = Pred (\a -> True) 

assert :: Contract a -> a -> a
assert (Pred p)       x = if p x then x else error "contract violation"
...

将它们放在一起，您会看到assert true x 将测试(\a -> True) x 并生成x 或抛出错误，具体取决于它是True 还是False。并且无论您对x 使用什么表达式，这将始终是True，因为根据定义，谓词始终返回True，并忽略其参数。

简单的解决方法是让true "contract" 实际测试其参数，如下所示：

true :: Contract Bool
true = Pred id

也就是说，这个新的true 只能应用于Bool 类型的值（因为它对其他任何人都没有任何意义）并且对它没有任何作用。如果它是True，它会让值保持不变，否则会抛出你想要的合约违规错误：

Prelude> assert true (5==6)
*** Exception: contract violation
CallStack (from HasCallStack):
  error, called at <interactive>:21:46 in interactive:Ghci2
Prelude> assert true (5==5)
True

并注意assert true (5==6) 中的括号，因为assert true 5==6 被解析为(assert true 5)==6，因为函数应用程序是Haskell 中最先例的“运算符”。 assert true 5==6 会导致错误，因为 true 的更正版本仅适用于布尔值，因此不适用于 5。

【讨论】：

【解决方案2】：

注意assert true x == x 将assert true x 与x 进行比较；所以assert true 5 是5，当然5 == 6 是假的，不是违反合同的。

如果您打算改为保留assert true (x == x)，那么看起来像

true :: Contract Bool
true = Pred id

assert true (5==6)  -- Contract violation

是你想要的

【讨论】：

【解决方案3】：

“当运行 assert true x == x 编译器说 x 未定义”在这里相当关键。在我看来，您的assert 调用是一个包含两个对x 的引用的表达式，最外层的函数是(==)。如果没有x 的绑定，任何一方都不能被评估。 assert true x 部分永远不会看到==，如果我们将其重写为assert true (x == x)，我们仍然需要提供x :: Eq a。我不知道如何检查这样的函数，但肯定有一些我不太熟悉的选项。

【讨论】：