read


read
or learn more

Clojure’s :pre and :post

Dec 21, 2009

One of the more exciting features of the upcoming Clojure 1.1 release is the inclusion of pre and post assertion functions. Some preliminary details can be found in the Clojure documentation, but I thought I’d quickly cover a simple example with potentially far-reaching implications; the case of making :post assertions relative to the input argument(s).

Let’s re-write the simple function constrained-sqr as found in the Clojure documentation linked above and re-cast it as constrained-fn:

(defn constrainedfn [f x]
  {:pre  [(pos? x)]
   :post [(= % (* 2 x))]}
  (f x))

(constrainedfn #(* 2 %) 2)
;=> 4
(constrainedfn #(float (* 2 %)) 2)
;=> 4.0
(constrainedfn #(* 3 %) 2)
;=> java.lang.Exception: Assert failed: (= % (* 2 x))

So what have I done? By specifying a :post assertion of (= % (* 2 x)) I’ve constrained the passed function f to be (effectively) a doubling function. I’ve done this by constraining the result of constrained-fn relative to its input. There is nothing entirely ground-breaking about pre and post conditions, but they are surprisingly powerful. By stripping out the assertions into a wrapper function I’ve detached some hairy logic from a potentially globally useful function and isolated it in an aspect (if you will) named constrained-fn. Now we could wrap the function f using a different constraining function depending on the context in which it is intended to be used; for example jimmys-fn, logged-result-fn, only-ints-fn, payroll-dept-fn, etc… In fact, I like that word aspect; it has a nice ring to it. I wonder if anyone has thought of that before?

-m

20 Comments, Comment or Ping

  1. Your post condition (= % (* 2 x)) constrains your function to be a “doubling” function, not a “squaring” function.

    I think you wanted this post condition: (= % (* x x))

  2. You are correct… the sad part is that I do not recall which one I actually wanted. I guess I’ll flip a coin. :-)

    Thank you -m

  3. Sean Devlin

    Hey, really cool post. I’d make a change to your wrapping fn

    (defn constrained-fn [f & args]
      {:pre  [(pos? (first args))]
       :post [(= % (* 2 (first args)))]}
      (apply f args))

    This way you can pass fns with multiple arguments and have them work correctly.

    Sean

  4. Is it just me, or is the fact they’re throwing java.lang.Exception’s rather than say AssertionException a little smelly.

  5. Yes, your apply version is good in that it moves further in the direction that I’d like to see :pre and :post evolve — that is, as elements of a more generic function overlay system. There is a current disparity in that the `:pre` and `:post` are specific to a particular “shape” of `f` while `(apply f args)` is generic.

    Thanks for reading.

    -m

  6. Do you mean java.lang.AssertionError? Good question. I can only speculate, but my guess is that throwing anything derived from java.lang.Error would be overkill. Seems like a fair question for http://groups.google.com/group/clojure.

    -m

  7. You might enjoy reading about PLT Scheme’s DbC system:

    http://docs.plt-scheme.org/guide/contract-boundaries.html

  8. You mentioned Gregor and Aspects but not Bertrand and DbC/Eiffel?

    Boo!

  9. mikhailfranco

    Have a look at this if you want to generalize ‘shape’

    http://conal.net/blog/posts/semantic-editor-combinators/

    Mik

  10. RE: Bertrand and Eiffel

    The omission was not intentional, but I didn’t want to mention other systems/langs that I couldn’t claim to know at least a little bit about. As for Eiffel — it keeps popping up during these :pre and :post discussions, so I suppose there is no way to postpone some deeper research. Thanks for the pointers.

    -m

  11. RE: Semantic Editors.

    Thanks for the link; I flagged this post a few days ago in my Zeitgeist-feed but haven’t had the chance to dig into it.

    -m

  12. @Rettke,

    Have I ever mentioned that PLT Scheme never ceases to amaze me? Well, I am now.

    -m

  13. Ivan Toshkov

    How is that better than what we have today?

    (defn constrained-fn [f x] (assert (pos? x)) (let [r (f x)] (assert (= r (* 2 x))) r))

    One can easily write a simple macro to handle the boilerplate.

  14. @Toshkov

    One advantage that :pre and :post have over assert is that the former allows the “assertions” to potentially come from a different source than the body of the function. This is what my example implies, even if I didn’t elucidate that exact point. :pre and :post also make it relatively easy to do some fancy automatic test generate and as a bonus provide a form of documentation for the function. Chris Houser added another interesting point that I was not aware of, “using assert instead of :pre is usually pretty straightforward, if you had to do it. Using assert instead of :post is a pain.” Sounds reasonable. Along that point, Chas Emerick’s assessment that :pre and :post cover 99.5% of assert uses, plus provide simple, and consistent hooks.

    Hope that helps. Thanks for reading.

    -m

  15. Alexander

    One thing that is always missed when people try to re-implement Eiffel’s design by contract is that the real strength of design by contract is how it interacts with polymorphism.

    In Clojure, :pre and :post should have been defined on generic functions where they shine.

    You don’t want simple :pre and :post, you want abstractions such as constrained-fn in the example above.

    In design by contract, constrained-fn should be a multi-method. The contract for constrained-fn should be that:

    Precondition: The argument should be positive, BUT CAN BE RELAXED.

    Postcondition: The result should be doubled, BUT CAN BE STRENGTHENED.

    Thus, preconditions should be combined by disjunction. Postconditions should be combined by conjunction.

    This should be done by the multi-method dispatch system. All preconditions for applicable functions should be ORed together and evaluated. The postconditions for all applicable functions should be ANDed together and evaluated.

    Why is this essential feature missed by everyone?

  16. @ Alexander

    Thanks for the great comment. There is much to ponder and there no longer and excuse for me to avoid Eifel.

    Thanks for reading.

    -m

  17. Michael: Thanks for posting this. It saves my runtime equivalent.

  18. Mamun

    I am just testing clojure :pre condition. But look like some case it is not working in clojure 1.5.1

    (defn check-keyword [v] {:pre [keyword? v]} v)

    (defn check-nil [v] {:pre [nil? v]} v)

    (check-keyword “sdf”) ;Not throwing exception here

    (check-nil nil) ;Throwing exception

    Br, Mamun

  19. @Mamun

    Your examples are missing some parentheses. When in doubt, add more. ;-)

    (defn check-keyword [v] {:pre [(keyword? v)]} v)
    (defn check-nil [v] {:pre [(nil? v)]} v)
    

    In your originals the reason that the second seemed to work is because v itself was nil. What I mean by that is Clojure takes the forms in the :pre/:post vector and evaluates them each in turn. If any of them is falsey then the assertion fails. In the case of (check-nil nil) you see that v takes on nil, Clojure evaluates that and indeed fails the assertion.

  20. DT

    Clojure throws AssertionError now (Clojure 1.10) on a failed condition.

    The thought occurs that the usability of a “postcondition runtime check” is severely curtailed once one starts returning lazy data structures … because you can’t examine them.

    Sufficiently annotated code and an actual theorem prover will have to take over at that point.

    P.S.

    The :post and :pre directives should be mentioned relatively early in “The Joy of Clojure 3rd edition” if it ever comes out – and be appropriately deployed in the examples.

    P.P.S.

    The image at the top of the page says JoC 2nd ed. is still in MEAP hell.

Reply to “Clojure’s :pre and :post”