fogus: Clojure’s :pre and :post

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 constrained-fn [f x]
  {:pre  [(pos? x)]
   :post [(= % (* 2 x))]}
  (f x))

(constrained-fn #(* 2 %) 2)
;=> 4
(constrained-fn #(float (* 2 %)) 2)
;=> 4.0
(constrained-fn #(* 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

Eric Lavigne

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))

Dec 21st, 2009
fogus

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

Dec 21st, 2009
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
Dec 21st, 2009
Mark Derricutt

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

Dec 21st, 2009
fogus

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

Dec 21st, 2009
fogus

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

Dec 21st, 2009
Grant Rettke

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

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

Dec 22nd, 2009
Grant Rettke

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

Boo!

Dec 22nd, 2009
mikhailfranco

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

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

Mik

Dec 22nd, 2009
fogus

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

Dec 22nd, 2009
fogus

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

Dec 22nd, 2009
fogus

@Rettke,

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

-m

Dec 22nd, 2009
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.

Dec 23rd, 2009
fogus

@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

Dec 23rd, 2009
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?

Dec 29th, 2009
fogus

@ 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

Dec 30th, 2009
octopusgrabbus

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

Aug 23rd, 2012
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

Feb 13th, 2014
fogus
@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.
Feb 13th, 2014
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.

Jun 29th, 2019

Send More Paramedics

Clojure’s :pre and :post

20 Comments, Comment or Ping

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