Есть ли укого сслыка на методику этого подхода и самое главное на примеры?

Здравствуйте, Аноним, Вы писали:

А>Есть ли укого сслыка на методику этого подхода и самое главное на примеры?

См. язык Эйфель / Eiffel (www.eiffel.com)

К>См. язык Эйфель / Eiffel (www.eiffel.com)

Спасибо!.а можно немного в общих словах перед началом чтения .в чем суть?

Здравствуйте, Аноним, Вы писали:

А>Спасибо!.а можно немного в общих словах перед началом чтения .в чем суть?

Контракт — это совокупность требований к тому, что будет на входе и что будет на выходе (а также — что в процессе).
То есть это декларативная составляющая императивного программирования.

В общих чертах: для каждого объекта и каждого действия объявляется ряд условий.
Например,

class counter
{
  int value;
  // invariant: 0 <= value < INT_MAX
public:
  counter() { reset(); }

  int now() const { return value; }

  void reset() { value=0; }
  // postcondition: value == 0

  // precondition: value < INT_MAX-1
  void step() { ++value; }
  // postcondion: value = old_value+1 && 1 <= value
};

// precondition: 0<x, 0<y
unsigned GCD(unsigned x, unsigned y) // НОД
{
  // тупым способом - алгоритм Эвклида

  // precondition: 0<x, 0<y
  while(x != y) // invariant: GCD(x,y) == GCD(original_x, original_y) && 0 < x && 0 < y
  {
    if(x > y)
      x -= y; // pre: x > y; post: x > 0
    else
      y -= x; // pre: y > x; post: y > 0
  }
  // postcondition: x == y == GCD(x,y) == GCD(original_x, original_y)
}
// postcondition: 1<=GCD(x,y)<min(x,y) && x % GCD(x,y) == y % GCD(x,y) == 0

т.е это верификая динамических свойств программы. спасибо больщое.