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?
