Badly formed pre/post conditions silently passed

Question

Before:


user=> ((fn [x] {:pre (pos? x)} x) -5) ; ouch!
-5
user=> ((fn [x] {:pre [(pos? x)]} x) -5) ; meant this
AssertionError Assert failed: (pos? x)  user/eval4075/fn--4076 (form-init5464179453862723045.clj:1)


After:


user=> ((fn [x] {:pre (pos? x)} x) -5)
CompilerException java.lang.IllegalArgumentException: Pre and post conditions should be vectors, compiling:(NO_SOURCE_PATH:1:2)
user=> ((fn [x] {:pre [(pos? x)]} x) -5)                                  
AssertionError Assert failed: (pos? x)  user/eval2/fn--3 (NO_SOURCE_FILE:2)
user=> ((fn [x] {:post (pos? x)} x) -5)
CompilerException java.lang.IllegalArgumentException: Pre and post conditions should be vectors, compiling:(NO_SOURCE_PATH:3:2)
user=> ((fn [x] {:post [(pos? x)]} x) -5)              
AssertionError Assert failed: (pos? x)  user/eval7/fn--8 (NO_SOURCE_FILE:4)


*Patch:* CLJ-1473_v03.patch
*Screened by:* Alex Miller

Answer 1

Comment made by: alexmiller

Would be nice to include the bad condition in the error (maybe via ex-info?) and also have tests.

Answer 2

Comment made by: bbloom

New patch includes tests. Unfortunately, can't call ex-info directly due to bootstrapping concerns. Instead, just calls ExceptionInfo constructor directly.

Answer 3

_Comment made by: alexmiller_

Bug in the reporting: {:post pre} should be {:post post}.

Test should be improved as it could have caught that.

Answer 4

Comment made by: bbloom

Good catch with the pre/post copy/paste screw up. Didn't enhance the test though, since that would involve creating an ex-info friendly variant of fails-with-cause

Answer 5

Comment made by: richhickey

:pre and :post don't require vectors, just collections

Answer 6

Comment made by: jafingerhut

Eastwood 0.2.2, released on Nov 15 2015, will warn about several kinds of incorrect pre and postconditions. See https://github.com/jonase/eastwood#wrong-pre-post

The Eastwood documentation may be misleading right now, in that it says that :pre and :post should be vectors, which is at odds with Rich's comment of Oct 9 2015. Corrections to Eastwood's documentation here are welcome. I guess Rich's intent is that :pre and :post could be vectors, lists, or sets? Would a map ever make sense there?

Answer 7

Comment made by: marco.m

Hello any news ?

Answer 8

_Comment made by: alexmiller_

There's feedback above from Rich that has never been addressed here. I took a stab at an update, but relaxing the constraint to just "collections of expressions" is kind of interesting. Once you do that, then the first example in the ticket here {:pre (pos? x)} is actually not invalid, it's a collection of two things: pos? and x. pos? evaluates to true (it's a function) and x evaluates to true for any number.

I'm not sure what the way forward is on that. It's perfectly valid and even potentially useful to refer to an incoming arg as a precondition, which would just be a symbol:


( (fn [v] {:pre [v]} v) nil)  ;; precondition should fail
( (fn [v] {:pre (v)} v) nil)  ;; equally valid


Maybe you could check for whether the elements of pre or post are either lists (expressions) or symbols that are arg bindings? Anything else is vacuously true and probably a bug. Not sure.

Answer 9

_Comment made by: jafingerhut_

Eastwood still gives warnings about code like the following:


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


Here is sample output:

src/filename.clj:5:22: wrong-pre-post: Precondition found that is probably always logical true or always logical false.  Should be changed to function call?  pos?

It also still warns if the value of :pre or :post is not a vector, despite Rich's comment, so it is overly strict in that sense, but maybe not so bad to be overly strict there.

Answer 10

Comment made by: martinklepsch

Just want to point to this PR (https://github.com/pedestal/pedestal/pull/544) as an example of how this affects production Clojure code.

Due to malformed pre/post conditions silently being accepted the API was essentially different from what the library authors intended. People started to rely on this and fixing the broken precondition essentially resulted in a breaking change.

Answer 11

Reference: https://clojure.atlassian.net/browse/CLJ-1473 (reported by bbloom)