I think it's a better idea, in some languages at least, to extend the signature to contain general preconditions and postconditions. public boolean doSomet

I think it's a better idea, in some languages at least, to extend the signature to contain general preconditions and postconditions. public boolean doSomethingFor(int iterations) { // this is considered part of the semantic signature requires iterations > 0 && iterations < 10; // implementation ... } Putting it in the types is a good idea, but extremely complicated. You need full dependent types to make it work.