不正确构造的预/后条件静默通过

Question

之前


user=> ((fn [x] {:pre (pos? x)} x) -5) ; ouch!
-5
user=> ((fn [x] {:pre [(pos? x)]} x) -5) ; 这才是我的意图
AssertionError 断言失败：(pos? x)  user/eval4075/fn--4076 (form-init5464179453862723045.clj:1)


之后


user=> ((fn [x] {:pre (pos? x)} x) -5)
编译器异常 java.lang.IllegalArgumentException: 预条件和后置条件应该是向量，编译：(NO_SOURCE_PATH:1:2)
user=> ((fn [x] {:pre [(pos? x)]} x) -5)                                  
AssertionError 断言失败：(pos? x)  user/eval2/fn--3 (NO_SOURCE_FILE:2)
user=> ((fn [x] {:post (pos? x)} x) -5)
编译器异常 java.lang.IllegalArgumentException: 预条件和后置条件应该是向量，编译：(NO_SOURCE_PATH:3:2)
user=> ((fn [x] {:post [(pos? x)]} x) -5)              
AssertionError 断言失败：(pos? x)  user/eval7/fn--8 (NO_SOURCE_FILE:4)


*补丁:* CLJ-1473_v03.patch
*审阅者:* Alex Miller

Answer 1

评论者：alexmiller

最好在错误（也许通过ex-info）中包含错误条件，并且还有测试。

Answer 2

评论者：bbloom

新补丁包含测试。不幸的是，由于引导问题无法直接调用ex-info。相反，只是直接调用ExceptionInfo构造函数。

Answer 3

由 alexmillerCommented:

报告中存在错误：{:post pre} 应为 {:post post}。

测试应该改进，因为它本可以捕捉到这一点。

Answer 4

评论者：bbloom

非常棒的发现，关于预/后条件复制粘贴错误。但没有增强测试，因为这需要创建一个对 ex-info 友好的 fails-with-cause 变体

Answer 5

由 richhickey Commented:

:pre 和 :post 不需要向量，只需要集合

Answer 6

由 jafingerhut Commented:

Eastwood 0.2.2 版本于2015年11月15日发布，将警告关于几种预和后条件的错误。详见 https://github.com/jonase/eastwood#wrong-pre-post

目前 Eastwood 的文档可能会导致误导，因为它说 :pre 和 :post 应该是向量，这与 Rich 2015 年10月9日的评论相矛盾。欢迎为 Eastwood 的文档进行修改。Rich 的意图是 :pre 和 :post 可以是向量、列表或集合吗？集合是否适合在那里使用？

Answer 7

由 marco.m Commented:

有什么新消息吗？

Answer 8

由 alexmillerCommented:

Rich 上面的反馈在此处尚未得到解答。我尝试了一个更新，但将约束放宽到仅为“表达式集合”有点很有趣。一旦这样做，这里的工单中第一个示例 {:pre (pos? x)} 实际上并不无效，它是一个两件事的集合：pos? 和 x。pos? 评估为真（它是一个函数），x 对任何数字都评估为真。

我不确定在这个问题上前进的方式是什么。将传入的参数用作前条件（即只是一个符号）是绝对有效甚至可能很有用的。


((fn [v] {:pre [v]} v) nil)  ;; 前条件应该失败
((fn [v] {:pre (v)} v) nil)  ;; 同样有效


也许你可以检查 pre 或 post 的元素是列表（表达式）还是符号参数绑定？否则可能是一个bug。不确定。

Answer 9

_由 jafingerhut 评论

Eastwood 仍然对如下代码发出警告


(defn foo [x]
  {:pre [pos? x]}
  (inc x))


以下是样本输出

src/filename.clj:5:22: wrong-pre-post: 找到的预条件可能总是逻辑上为真或为假。  应更改为函数调用？  pos?

即使 Rich 有评论，它仍然会警告 :pre 或 :post 的值不是向量，因此在这一点上它过于严格，但也许不是过于严格。

Answer 10

由 martinklepsch 评论

只想指出这个 PR (https://github.com/pedestal/pedestal/pull/544) 作为此问题如何影响生产 Clojure 代码的示例。

由于未正确形成的 pre/post 条件无声地被接受，API 实质上与库作者意图的不同。人们开始依赖于它，修复损坏的预条件实际上导致了一次重大更改。

Answer 11

参考：https://clojure.atlassian.net/browse/CLJ-1473（由 bbloom 报告）