Есть ли укого сслыка на методику этого подхода и самое главное на примеры?
Здравствуйте, Аноним, Вы писали:
А>Есть ли укого сслыка на методику этого подхода и самое главное на примеры?
См. язык Эйфель / 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
т.е это верификая динамических свойств программы. спасибо больщое.