The D programming language includes language support for design-by-contract but, unlike SPARK, it's a sane language. (It's C++ without the suck and with some more modern features.) I'm still investigating it, and it's still under development , but I strongly recommend checking it out, C++ fan or not.
Here's a (necessarily trivial) example, taken from the website:
long square_root(long x) in { assert(x >= 0); } out (result) { assert((result * result) == x); } body { return math.sqrt(x); }
Here's a (necessarily trivial) example, taken from the website: