If the time bound is being put in place in the hopes of being able to automatically analyze the behaviour of the code, then no.

I singled out "outputting 0" on every input because it's among the simplest possible specs you could try try to check with the kind of "very powerful semantic analysis" tool the top-level post was hoping for. In practice you probably want to check a more complex spec -- you want your code to solve a specific problem on whatever input it receives -- but if the "always output 0" spec is impossible to automatically check, then what hope do more relevant specs have?