Eiffel
Object-oriented language built around Design by Contract — preconditions, postconditions, and invariants are first-class language features.
static
compiled
since 1985
oopimperative
Eiffel introduced Design by Contract as a first-class language feature — methods declare preconditions they expect, postconditions they guarantee, and class invariants that must always hold. Violations are caught at runtime with precise diagnostics. Its concepts directly influenced the assert and ensure patterns in many languages and formal methods research.