Check out D (Score 1)

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