Do assertions provide a mechanism for subtyping? If not are they composable?

[Jonathan]

D allows inputs and outputs to have assertions placed on them.

i.e.

int f(int x){
   in{
     assert(even(x));
   }
   out{
     assert(odd(x));;
   }
}

I would like to know if D tries to statically check these 
assertions.  If so that would give a subtyping mechanism which 
would be kind of neat.

If not, consider the following scenario in addition to f.

int g(int x){
   in{
     assert(!odd(x));
   }
  ...
}

Suppose I made a call:

   g(f(x));

Can this be made to fail by composing the assertions?

Are there any tools or support for model checking and/or software 
verification in D outside of the core language (like Frama-C) 
that would support such analyses?