какие выходные данные подпрограмма считает

integer_division(dividend, divisor, result, remainder: INTEGER) is

     require

         divisor > 0

  do

     from

          result = 0; remainder = dividend;

     invariant

          dividend = result*divisor + remainder

     variant

          remainder

     until

          remainder < divisor

     loop



          remainder := remainder - divisor;

          result := result + 1 ;

     end

   ensure

      dividend = result*divisor + remainder;

       remainder < divisor

end

     Конструкция require (требуется) называется предусловием и специ­фицирует, какие выходные данные подпрограмма считает правильными. Конструкция do (выполнить) содержит выполняемые операторы, собственно и составляющие программу. Конструкция ensure (гарантируется) называется постусловием и содержит. условия, истинность которых подпрограмма обещает обеспечить, если будет выполнена конструкция do над данными, удовлетворяющими предусловию. В данном случае справедливость постус­ловия является достаточно тривиальным следствием инварианта (см. 6.6) и условия until.

      На большем масштабе вы можете присоединить инвариант к классу (см. раздел 15.4). Например, класс, реализующий стек с помощью массива, вклю­чал бы инвариант такого вида:

invariant

   top >= 0;

   top < max;

Все подпрограммы класса должны гарантировать, что инвариант истинен, когда объект класса создан, и что каждая подпрограмма сохраняет истиность инварианта. Например, подпрограмма pop имела бы предусловие top> 0, в противном случае выполнение оператора:

top := top - 1

могло бы нарушить инвариант.

 

 

Типы перечисления

 

Инварианты применяются также, чтобы гарантировать безопасность типа, которая достигается в других языках использованием типов перечисления. Следующие объявления в языке Ada:

Ada

type Heat is (Off, Low, Medium, High);

Dial: Heat;

были бы записаны на языке Eiffel как обычные целые переменные с имено­ванными константами:


Содержание раздела

---