Контрактное проектирование

Контракты используются в программировании чтобы сформулировать ожидания. Виды параметров подпрограммы можно рассматривать как простую форму контрактов. Когда спецификация подпрограммы Op объявляет параметр, вида in, вызывающий Op знает, что аргумент in не будет изменен Op. Другими словами, вызывающий ожидает, что Op не изменяет предоставляемый им аргумент, а просто читает информацию, хранящуюся в аргументе. Ограничения и подтипы являются другими примерами контрактов. В целом, эти спецификации улучшают согласованность приложения.

Контрактное программирование основывается на таких техниках, как указание пред- и постусловий, предикатов подтипов и инвариантов типов. Мы изучаем эти темы в этой главе.

Пред- и постусловия

Пред- и постусловия формализируют ожидания относительно входных и выходных параметров подпрограмм и возвращаемого значения функций. Если мы говорим, что некие требования должны быть выполнены перед вызовом подпрограммы Op, это предварительные условия. Точно так же, если определенные требования должны быть выполнены после вызова подпрограммы Op, это постусловия. Мы можем думать о предусловиях и постусловиях как об обещаниях между тем, кто вызывает и тем, кто принимает вызов подпрограммы: предусловие - это обещание от вызывающего к вызываемому, а постусловие - это обещание в обратном направлении.

Пред- и постусловия указываются с помощью спецификации аспекта в объявлении подпрограммы. Спуцификация with Pre => <условие> определяет предварительное условие, а спецификация with Post => <условие> определяет постусловие.

В следующем коде показан пример предварительных условий:

procedure Show_Simple_Precondition is procedure DB_Entry (Name : String; Age : Natural) with Pre => Name'Length > 0 is begin -- Missing implementation null; end DB_Entry; begin DB_Entry ("John", 30); -- Precondition will fail! DB_Entry ("", 21); end Show_Simple_Precondition;

show_simple_precondition.adb

Enable tabbed editor view for this editor Use the dark theme

Run

В этом примере мы хотим, чтобы поле имени в нашей базе данных не содержало пустой строки. Мы реализуем это требование, используя предварительное условие, требующее, чтобы длина строки, используемой для параметра Name процедуры DB_Entry, была больше нуля. Если процедура DB_Entry вызывается с пустой строкой для параметра Name, вызов завершится неудачно, поскольку предварительное условие не выполнено.

В наборе инструментов GNAT

GNAT обрабатывает предварительные и постусловия, генерируя код для проверки утверждений (assertion) во время выполнения программы. Однако по умолчанию проверка утверждения не включена. Следовательно, чтобы проверять предварительные и постусловия во время выполнения, вам необходимо включить проверку утверждений с помощью ключа -gnata.

Прежде чем мы перейдем к следующему примеру, давайте кратко обсудим кванторные выражения, которые весьма полезны для краткого написания предварительных и постусловий. Кванторные выражения возвращают логическое значение, указывающее, соответствуют ли элементы массива или контейнера ожидаемому условию. Они имеют форму: (for all I in A'Range => <условие для A(I)>, где A - это массив, а I - индекс. Кванторные выражения, использующие for all, проверяют, выполняется ли условие для каждого элемент. Например:

(for all I in A'Range => A (I) = 0)

Это кванторные выражение истинно только тогда, когда все элементы массива A имеют нулевое значение.

Другой вид кванторных выражений использует for some. Он выглядит примерно так: (for some I in A'Range => <условие для A(I)>. И в этом случае кванторное выражение проверяет, есть ли некоторые (some) элементы (отсюда и название) для которых условие истино.

Проиллюстрируем постусловия на следующем примере:

with Ada.Text_IO; use Ada.Text_IO; procedure Show_Simple_Postcondition is type Int_8 is range -2 ** 7 .. 2 ** 7 - 1; type Int_8_Array is array (Integer range <>) of Int_8; function Square (A : Int_8) return Int_8 is (A * A) with Post => (if abs A in 0 | 1 then Square'Result = abs A else Square'Result > A); procedure Square (A : in out Int_8_Array) with Post => (for all I in A'Range => A (I) = A'Old (I) * A'Old (I)) is begin for V of A loop V := Square (V); end loop; end Square; V : Int_8_Array := (-2, -1, 0, 1, 10, 11); begin for E of V loop Put_Line ("Original: " & Int_8'Image (E)); end loop; New_Line; Square (V); for E of V loop Put_Line ("Square: " & Int_8'Image (E)); end loop; end Show_Simple_Postcondition;

show_simple_postcondition.adb

Enable tabbed editor view for this editor Use the dark theme

Run

Мы объявляем 8-битный тип со знаком Int_8 и массив элементов этого типа (Int_8_Array). Мы хотим убедиться, что после вызова процедуры Square каждый элемент массива Int_8_Array возведен в квадрат. Мы делаем это с помощью постусловия, используя выражение for all. Это постусловие использует атрибут 'Old чтобы сослаться на исходное (до вызова) значение параметра.

Мы также хотим убедиться, что результат вызовов функции Square больше, чем аргумент этого вызова. Для этого мы пишем постусловие, применяя атрибут 'Result к именем функции и сравниваем его с входным значением.

Мы можем использовать как предварительные, так и постусловия в объявлении одной подпрограммы. Например:

with Ada.Text_IO; use Ada.Text_IO; procedure Show_Simple_Contract is type Int_8 is range -2 ** 7 .. 2 ** 7 - 1; function Square (A : Int_8) return Int_8 is (A * A) with Pre => (Integer'Size >= Int_8'Size * 2 and Integer (A) * Integer (A) <= Integer (Int_8'Last)), Post => (if abs A in 0 | 1 then Square'Result = abs A else Square'Result > A); V : Int_8; begin V := Square (11); Put_Line ("Square of 11 is " & Int_8'Image (V)); -- Precondition will fail... V := Square (12); Put_Line ("Square of 12 is " & Int_8'Image (V)); end Show_Simple_Contract;

show_simple_contract.adb

Enable tabbed editor view for this editor Use the dark theme

Run

В этом примере мы хотим убедиться, что входной аргумент вызовова функции Square не вызовет переполнения типа Int_8 в нашей функции. Мы делаем это путем преобразования входного значения в тип Integer, который используется для промежуточных вычислений, и проверяем, находится ли результат в допустимом для типа Int_8 диапазоне. В этом примере у нас то же постусловие, что и в предыдущем.

Предикаты

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

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

Статические и динамические предикаты указываются с помощью следующих спецификаций:

• with Static_Predicate => <свойство>

• with Dynamic_Predicate => <свойство>

Давайте воспользуемся следующим примером, чтобы проиллюстрировать динамические предикаты:

with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with Ada.Calendar; use Ada.Calendar; with Ada.Containers.Vectors; procedure Show_Dynamic_Predicate_Courses is package Courses is type Course_Container is private; type Course is record Name : Unbounded_String; Start_Date : Time; End_Date : Time; end record with Dynamic_Predicate => Course.Start_Date <= Course.End_Date; procedure Add (CC : in out Course_Container; C : Course); private package Course_Vectors is new Ada.Containers.Vectors (Index_Type => Natural, Element_Type => Course); type Course_Container is record V : Course_Vectors.Vector; end record; end Courses; package body Courses is procedure Add (CC : in out Course_Container; C : Course) is begin CC.V.Append (C); end Add; end Courses; use Courses; CC : Course_Container; begin Add (CC, Course'( Name => To_Unbounded_String ("Intro to Photography"), Start_Date => Time_Of (2018, 5, 1), End_Date => Time_Of (2018, 5, 10))); -- This should trigger an error in the -- dynamic predicate check Add (CC, Course'( Name => To_Unbounded_String ("Intro to Video Recording"), Start_Date => Time_Of (2019, 5, 1), End_Date => Time_Of (2018, 5, 10))); end Show_Dynamic_Predicate_Courses;

show_dynamic_predicate_courses.adb

Enable tabbed editor view for this editor Use the dark theme

Run

В этом примере пакет Courses определяет тип Course и тип Course_Container, объект которого содержит все курсы. Мы хотим обеспечить согласованность дат каждого курса, в частности, чтобы дата начала была не позже даты окончания. Чтобы обеспечить соблюдение этого правила, мы объявляем динамический предикат для типа Course, который будет действовать для каждого объекта. Предикат использует имя типа, так как будь-то это обычная переменная данного типа: такое имя обозначает экземпляр проверяемого объекта.

Обратите внимание, что в приведенном выше примере используются неограниченные строки и даты. Оба типа доступны в стандартной библиотеке Ада. Пожалуйста, обратитесь к следующим разделам для получения дополнительной информации:

• о типе неограниченной строки (Unbounded_String): раздел Неограниченные строки;

• о дате и времени: Раздел Даты и время.

Статические предикаты, как упоминалось выше, в основном используются для скалярных типов и проверяются во время компиляции. Они особенно полезны для представления несмежных элементов перечисления. Классический пример - список дней недели:

type Week is (Mon, Tue, Wed, Thu, Fri, Sat, Sun);

Мы можем легко создать подсписок рабочих дней в неделе, указав подтип (subtype) с диапазоном на основе Week. Например:

subtype Work_Week is Week range Mon .. Fri;

Диапазоны в Аде могут быть указаны только как непрерывные списки: они не позволяют нам выбирать определенные дни. Однако нам может понадобиться создать список, содержащий только первый, средний и последний день рабочей недели. Для этого мы используем статический предикат:

subtype Check_Days is Work_Week
  with Static_Predicate => Check_Days in Mon | Wed | Fri;

Давайте посмотрим на полный пример:

with Ada.Text_IO; use Ada.Text_IO; procedure Show_Predicates is type Week is (Mon, Tue, Wed, Thu, Fri, Sat, Sun); subtype Work_Week is Week range Mon .. Fri; subtype Test_Days is Work_Week with Static_Predicate => Test_Days in Mon | Wed | Fri; type Tests_Week is array (Week) of Natural with Dynamic_Predicate => (for all I in Tests_Week'Range => (case I is when Test_Days => Tests_Week (I) > 0, when others => Tests_Week (I) = 0)); Num_Tests : Tests_Week := (Mon => 3, Tue => 0, Wed => 4, Thu => 0, Fri => 2, Sat => 0, Sun => 0); procedure Display_Tests (N : Tests_Week) is begin for I in Test_Days loop Put_Line ("# tests on " & Test_Days'Image (I) & " => " & Integer'Image (N (I))); end loop; end Display_Tests; begin Display_Tests (Num_Tests); -- Assigning non-conformant values to -- individual elements of the Tests_Week -- type does not trigger a predicate -- check: Num_Tests (Tue) := 2; -- However, assignments with the "complete" -- Tests_Week type trigger a predicate -- check. For example: -- -- Num_Tests := (others => 0); -- Also, calling any subprogram with -- parameters of Tests_Week type -- triggers a predicate check. Therefore, -- the following line will fail: Display_Tests (Num_Tests); end Show_Predicates;

show_predicates.adb

Enable tabbed editor view for this editor Use the dark theme

Run

Здесь у нас есть приложение, которое хочет проводить тесты только три дня в рабочей неделе. Эти дни указаны в подтипе Test_Days. Мы хотим отслеживать количество тестов, которые проводятся каждый день. Мы объявляем тип Tests_Week как массив, объект которого будет содержать количество тестов, выполняемых каждый день. Согласно нашим требованиям, эти тесты должны проводиться только в вышеупомянутые три дня; в другие дни никаких анализов проводить не следует. Это требование реализовано с помощью динамического предиката типа Tests_Week. Наконец, фактическая информация об этих тестах хранится в массиве Num_Tests, который является экземпляром типа Tests_Week.

Динамический предикат типа Tests_Week проверяется во время инициализации Num_Tests. Если у нас там будет несоответствующее значение, проверка не удастся. Однако, как мы видим в нашем примере, изменения отдельных элементов массива не приводят к выполнению проверки. Так происходит потому, что инициализация сложной структуры данных (например, массивов или записей) может требовать выполнения нескольких операций присваивания. Однако, как только объект передается в качестве аргумента подпрограмме, динамический предикат проверяется, потому что подпрограмма требует, чтобы объект был согласован. Это происходит при вызове Display_Tests в последнем операторе нашего примера. Здесь проверка предиката вызовет ошибку потому, что предыдущее изменение приводит к несогласованному значению.

Инварианты типа

Инварианты типов - это еще один способ определить ожидания относительно типов. В то время как предикаты используются для всех типов, инварианты типов используются исключительно для определения ожиданий в отношении личных типов. Если тип T из пакета P имеет инвариант типа, результаты операций с объектами типа T всегда согласуются с этим инвариантом.

Инварианты типов указываются с помощью предложения with Type_Invariant => <свойство>. Подобно предикатам, свойство определяет условие, которое позволяет нам контролировать, соответствует ли объект типа T нашим требованиям. В этом смысле инварианты типов можно рассматривать как своего рода предикаты для личных типов. Однако есть некоторые отличия касающиеся проверок. Эти отличия приведены в следующей таблице:

Элемент	Проверки параметров подпрограммы	Проверки присвоения
Предикаты	По всем входящим in и выходящим out параметрам	При присваивании и явных инициализациях
Инварианты типов	По параметрам out, возвращенным из подпрограмм, объявленных в том же видимом разделе	При всех инициализациях

Мы могли бы переписать наш предыдущий пример и заменить динамические предикаты инвариантами типов. Это выглядело бы так:

with Ada.Text_IO; use Ada.Text_IO; with Ada.Strings.Unbounded; use Ada.Strings.Unbounded; with Ada.Calendar; use Ada.Calendar; with Ada.Containers.Vectors; procedure Show_Type_Invariant is package Courses is type Course is private with Type_Invariant => Check (Course); type Course_Container is private; procedure Add (CC : in out Course_Container; C : Course); function Init (Name : String; Start_Date, End_Date : Time) return Course; function Check (C : Course) return Boolean; private type Course is record Name : Unbounded_String; Start_Date : Time; End_Date : Time; end record; function Check (C : Course) return Boolean is (C.Start_Date <= C.End_Date); package Course_Vectors is new Ada.Containers.Vectors (Index_Type => Natural, Element_Type => Course); type Course_Container is record V : Course_Vectors.Vector; end record; end Courses; package body Courses is procedure Add (CC : in out Course_Container; C : Course) is begin CC.V.Append (C); end Add; function Init (Name : String; Start_Date, End_Date : Time) return Course is begin return Course'(Name => To_Unbounded_String (Name), Start_Date => Start_Date, End_Date => End_Date); end Init; end Courses; use Courses; CC : Course_Container; begin Add (CC, Init (Name => "Intro to Photography", Start_Date => Time_Of (2018, 5, 1), End_Date => Time_Of (2018, 5, 10))); -- This should trigger an error in the -- type-invariant check Add (CC, Init (Name => "Intro to Video Recording", Start_Date => Time_Of (2019, 5, 1), End_Date => Time_Of (2018, 5, 10))); end Show_Type_Invariant;

show_type_invariant.adb

Enable tabbed editor view for this editor Use the dark theme

Run

Основное отличие состоит в том, что в предыдущем примере тип Course был полностью описан в видимом разделе пакета Courses, но в этом примере он является личным типом.