CODEWITHSUNDEEP
code-contractsdesign-by-contract
user1004413
user1004413

Reputation: 2629

Views on Design By Contract or code contract

I am currently reading up to understand more about Design By contract / code contract.

As from what i know, it is to write contracts (Invariants, Pre and Post conditions) to ensure that the codes can be maintain orderly. It will also guarantees that bugs will be prevented by a well defined mechanism based on checks and balances

But wouldnt this implicated the software performance? As there are additional checks between each method calls.

I will really appreciate people to share their views and experience with Design By Contract with me. Disadvantages or advantages are welcome.

Upvotes: 3

Views: 198

Answers (3)

Bert F
Bert F

Reputation: 87553

Design-by-contract is intended to ensure correct implementation - that the code is written correctly with respect to the intended API between caller and callees. Ideally, you verify the contracts are upheld using static analysis tools and runtime checks in development and alpha test environments. Hopefully by then you have caught any implementation errors with respect to API errors. You probably don't use the runtime checks for beta and production unless you are trying to track down an error.

Upvotes: 0

Pascal Cuoq
Pascal Cuoq

Reputation: 80305

One way to apply the design-by-contract philosophy is purely static. Consider a contract for a function max_element():

/*@
requires IsValidRange(a, n);
assigns \nothing;
behavior empty:
assumes n == 0; ensures \result == 0;
behavior not_empty:
assumes 0 < n;
ensures 0 <= \result < n;
ensures \forall integer i; 0 <= i < n ==> a[i] <= a[\result]; ensures \forall integer i; 0 <= i < \result ==> a[i] < a[\result];
complete behaviors;
disjoint behaviors;
*/
size_type max_element(const value_type* a, size_type n);

If you are able to verify at compile-time that an implementation always guarantees that the post-conditions in the ensures clauses are satisfied provided that the function is called with arguments that satisfy the pre-conditions in the requires clauses, it is unnecessary to generate checks for the post-conditions.

Similarly, if you verify that all the callers, when their own pre-conditions are satisfied, call max_element() only with arguments that satisfy its pre-conditions, then the checks are unnecessary at the entry of the function.

The above example is from ACSL by Example. This library provides many function contracts in ACSL. Implementations in C are provided for the contracts. The implementations have been statically formally verified to guarantee that the post-conditions hold for all calls with arguments that satisfy the pre-conditions. Therefore, no run-time check is necessary for the post-conditions. The compiler can treat the annotations as comments (which they are, using the /*@ ... */ syntax).

Upvotes: 1

Olly
Olly

Reputation: 6026

Typically such frameworks support runtime checks and static ananlysis. The latter is performed at compile time (or before); it does not slow down your code at all. The former could potentially affect performance.

The Microsoft Research Code Contracts project is a nice example of this. You can configure your system such that:

  • static analysis applies a subset of the possible contract enforcement at compile time, or even within the deigner environment;

  • runtime checks are enabled for all code compiled in debug mode; and

  • a subset of the runtime checks is enabled for the public API of code compiled in release mode (non-public code has no runtime checks).

This is often a good compromise between performance and robustness.

Upvotes: 3

Related Questions