Contract-based programming is a software development technique, which is used to find programming errors earlier in the development process. "Contract" refers to formal declarations of how types and subprograms ("functions and methods" if you aren't an Ada programmer already) behave. In the strictest form, the contracts are checked as a part of the compilation process, and only a program which can be proven to conform with the contracts will compile. In a less strict form, it is more similar to "preventive debugging", where the contracts are inserted as run-time checks, which makes it more likely to identify errors during testing.

Ada provides a quite extensive support for contract-based programming. The checks are specified as a mix of compile-time checks, obligatory run-time checks, and optional run-time checks. In addition to that, SPARK defines a subset of Ada with full compile-time checks.