Design by contract is based on Hoare logic where a proof of correctness of a program is established by reasoning over pre/post conditions and invariants.
What are the means and prerequisites of a language that make such reasoning possible?
Can it be checked statically or is it only a form of runtime assertion?
Answering your first question there seems to be no obstacle to design or extend a language to support DbC. However DbC introduces not just assertions to a language, but also a set of rules that tell how to combine these assertions in presence of (multiple) inheritance and redeclarations. As a result simple annotations cannot be easily translated into executable code unless the language tools are aware how to do it.
As to the second question, originally Design by Contract™ was introduced in Eiffel and was indeed meant for run-time checks. Over time there have been some changes and I'll mention only some of them:
Regular compilation. For some time Eiffel features so called void-safety, i.e. a guarantee that there is never a call on Void target (i.e. exceptions of type NullReferenceException are impossible). This technology relies on some rules. In order to make void-safe programming feasible and close to a regular programmer reasoning they involve assertions in a certain form. For example, methods that trigger exceptions have postconditions in the form False to indicate that any code after the calls to such methods is unreachable. The compiler then knows that there is no reason to check void-safety rules after such calls because it will never be executed.
Test generation. Preconditions and postconditions may serve as a good base to generate tests automatically, just by looking at the specification. This technology is a mix of both static and dynamic approaches, when static analysis takes part in test generation and test execution checks assertions at run-time. An example of such a tool is AutoTest.
Code verification. Some verification tools for different languages rely on DbC specifications to prove correctness. For Java it is JML, for Eiffel - AutoProof. On the current web page of the latter you can find a link to an online version that provides some examples where you can try to figure out what's wrong in the sample code and to fix it. It exploits DbC and uses some model classes to rigorously describe behavior of containers in the form of normal pre- and postconditions. The analysis is completely static, i.e. if the tool says that all assertions are satisfied, there will be no assertion violations at run-time and assertions checks can be safely turned off.
