Безопасная архитектура
Если говорить о строительстве, то хорошей архитектурой считается та, что гарантирует требуемую прочность самым естественным и простейшим путем, предоставляя людям безопасную среду обитания. Красивым примером может служить Пантеон в Риме, чья сферическая форма обладает чрезвычайной прочностью и в тоже время предоставляет максимум свободного пространства. Многие кафедральные соборы не так хороши и нуждаются в дополнительных колоннах снаружи для поддержки стен. В 1624г. сэр Ганри Вутон подытожил эту тему следующими словами: «хорошее строение удовлетворяет трем условиям - удобство, прочность и красота».
Аналогично, хорошая архитектура в программировании должна обеспечивать безопасность функционирования отдельных компонент простейшим образом, при этом сохраняя прозрачность системы в целом. Она должна обеспечивать взаимодействие, где это необходимо, и препятствовать взаимному влиянию действий, не связанных друг с другом. Хороший язык программирования должен позволять писать эстетически красивые программы с хорошей архитектурой.
Возможно, здесь есть аналогия с архитектурой офисных помещений. Если выделить каждому отдельный кабинет, это будет препятствовать общению и обмену идеями. С другой стороны, полностью открытое пространство приведет к тому, что шум и другие отвлекающие факторы будут препятствовать продуктивной работе.
Структура программ на Аде базируется на идее пакетов, которые позволяют сгруппировать взаимосвязанные понятия и предоставляют очевидный способ сокрытия деталей реализации.
Спецификация и тело пакета
Ранние языки программирования, такие как FORTRAN, имели плоскую структуру, где все располагалось, в основном, на одном уровне. Как следствие, все данные (не считая локальных данных подпрограммы) были видимы всюду. Это похоже на единое открытое пространство в офисе. Похожую плоскую модель предлагает и язык C, хотя и предлагает некоторую дополнительную возможность инкапсуляции, предоставляя программисту возможность контролировать видимость подпрограмм за границами текущего файла.
Другие языки, например Algol и Pascal, имеют простую вложенную блочную структуру, напоминающую матрешку. Это немного лучше, но все равно напоминает единое открытое пространство, поделенное на отдельные мелкие офисы. Проблема взаимодействия все равно остается.
Рассмотрим стек из чисел в качестве простого примера. Мы хотим иметь протокол, позволяющий добавить элемент в стек, используя вызов процедуры Push, и удалить верхний элемент, используя функцию Pop. И, допустим, еще одну процедуру Clear для сброса стека в пустое состояние. Мы намерены предотвратить все другие способы модификации стека, чтобы сделать данный протокол независимым от метода его реализации.
Рассмотрим реализацию, написанную на Pascal-е. Для хранения данных используется массив, а для работы написаны три подпрограммы. Константа max ограничивает максимальный размер стека. Это позволяет нам избежать дублирования числа 100 в нескольких местах, на тот случай, если нам потребуется его изменить.
const max = 100;
var top : 0 .. max;
a : array [1..max] of real;
procedure Clear;
begin
top := 0
end;
procedure Push(x : real);
begin
top := top + 1;
a[top] := x
end;
function Pop : real;
begin
top := top - 1;
Pop := a[top+1]
end;
Главная проблема тут в том, что max, top и a должны быть объявлены вне подпрограмм Push, Pop и Clear, чтобы мы могли иметь доступ к ним. Как следствие, в любом месте программы, где мы можем вызвать Push, Pop и Clear, мы также можем непосредственно поменять top и a, обойдя, таким образом протокол использования стека и получить несогласованное состояние стека.
Это может служить источником проблем. Если нам захочется вести учет количества изменений стека, то просто добавить счетчик в процедуры Push, Pop и Clear может оказаться недостаточно. При анализе большой программы, когда нам нужно найти все места, где стек изменялся, нам нужно отследить не только вызовы Push, Pop и Clear, но и обращения к переменным top и a.
Аналогичная проблема существует и в C и в Fortran. Эти языки пытаются ее преодолеть, используя механизм раздельной компиляции. Объекты, видимые из других единиц компиляции, помечаются специальной инструкцией extern либо при помощи заголовочного файла. Однако, проверка типов при пересечении границ модулей компиляции в этих языках работает гораздо хуже.
Язык Ада предлагает использовать механизм пакетов, чтобы защитить данные, используемые в Push, Pop и Clear от доступа извне. Пакет делится на две части — спецификацию, где описывается интерфейс доступный из других модулей, и тело, где располагается реализация. Другими словами, спецификация задает что делать, а тело — как это делать. Спецификация стека могла бы быть следующей:
package Stack is
procedure Clear;
procedure Push (X : Float);
function Pop return Float;
end Stack;
Здесь описан интерфейс с внешним миром. Т.е. вне пакета доступны лишь три подпрограммы. Этой информации достаточно программисту, чтобы вызывать нужные подпрограммы, и достаточно компилятору, чтобы эти вызовы скомпилировать. Тело пакета может иметь следующий вид:
package body Stack is
Max : constant := 100;
Top : Integer range 0 .. Max := 0;
A : array (1 .. Max) of Float;
procedure Clear is
begin
Top := 0;
end Clear;
procedure Push (X : Float) is
begin
Top := Top + 1;
A (Top) := X;
end Push;
function Pop return Float is
begin
Top := Top - 1;
return A (Top + 1);
end Pop;
end Stack;
Тело содержит полный текст подпрограмм, а также определяет скрытые объекты Max, Top и A. Заметьте, что начальное значение Top равняется нулю.
Для того, чтобы использовать сущности, описанные в пакете, клиентский код должен указать пакет в спецификаторе контекста (с помощью зарезервированного слова with) следующим образом:
with Stack;
procedure Some_Client is
F : Float;
begin
Stack.Clear;
Stack.Push (37.4);
...
F := Stack.Pop;
...
Stack.Top := 5; -- Ошибка!
end Some_Client;
Теперь мы уверены, что требуемый протокол будет соблюден. Клиент (программный код, использующий пакет) не может ни случайно, ни намеренно взаимодействовать с деталями реализации стека. В частности, прямое присваивание значения Stack.Top запрещено, поскольку переменная Top не видима для клиента (т. к. о ней нет упоминания в спецификации пакета).
Обратите внимание на три составляющие этого примера: спецификацию пакета, тело пакета и клиента.
Существуют важные правила, касающиеся их компиляции. Клиент не может быть скомпилирован пока не будет предоставлена спецификация. Тело также не может быть скомпилировано без спецификации. Но подобных ограничений нет между телом и клиентом. Если мы решим изменить детали реализации и это не затрагивает спецификацию, то в перекомпиляции клиента нет нужды.
Пакеты и подпрограммы верхнего уровня (т. е. не вложенные в другие подпрограммы) могут быть скомпилированы раздельно. Их обычно называют библиотечными модулями и говорят, что они находятся на уровне библиотеки.
Заметим, что пакет Stack упоминается каждый раз при обращении к его сущностям. В результате в коде клиента наглядно видно, что происходит. Но если постоянное повторение имени пакета напрягает, можно использовать спецификатор использования (с помощью служебного слова use):
with Stack; use Stack;
procedure Client is
begin
Clear;
Push (37.4);
...
end Client;
Однако, если используются два пакета, например Stack1 и Stack2, каждый из которых определяют подпрограмму Clear, и мы используем with и use для обоих, то код будет неоднозначным и компилятор не примет его. В этом случае достаточно указать необходимый пакет явно, например Stack2.Clear.
Подытожим вышесказанное. Спецификация определяет контракт между клиентом и пакетом. Тело пакета обязано реализовать спецификацию, а клиент обязан использовать пакет только указанным в спецификации образом. Компилятор проверяет, что эти обязательства выполняются. Мы вернемся к этому принципу позже в данной главе, а также в последней главе, когда рассмотрим поддержку контрактного программирования в Аде 2012 и идеи, лежащие в основе инструментария SPARK соответственно.
Дотошный читатель отметит, что мы полностью игнорировали ситуации переполнения (вызов Push при Top = Max) и исчерпания (вызов Pop при Top = 0) стека. Если одна из подобных неприятностей случиться, сработает проверка диапазона значения Top и будет возбужденно исключение Constraint_Error. Было бы хорошо включить предусловия для вызова подпрограмм Push и Pop в их спецификацию в явном виде. Тогда при использовании пакета программист бы знал, чего ожидать от вызова подпрограмм. Такая возможность появилась в Ада 2012, как часть поддержки технологии контрактного программирования, мы далее обсудим это.
Исключительно важным моментом здесь является то, что в Аде контроль строгой типизации не ограничен границами модулей компиляции. Написана ли программа как один компилируемый модуль или состоит из нескольких модулей, поделенных на разные файлы, производимые проверки будут совпадать в точности.
Приватные типы
Еще одна возможность пакета позволяет спрятать часть спецификации от клиента. Это делается при помощи так называемой приватной части. В примере выше пакет Stack реализует лишь один стек. Возможно, будет полезнее написать такой пакет, чтобы он позволял определить множество стеков. Чтобы достичь этого, нам нужно ввести понятие стекового типа. Мы могли бы написать
package Stacks is
type Stack is private;
procedure Clear (S : out Stack);
procedure Push (S : in out Stack; X : in Float);
procedure Pop (S : in out Stack; X : out Float);
private
Max : constant := 100;
type Vector is array (1 .. 100) of Float;
type Stack is record
A : Vector;
Top : Integer range 0 .. Max := 0;
end record;
end Stacks;
Это очевидное обобщение одно-стековой версии. Но стоит отметить, что в Аде 2012 появляется выбор, описать Pop либо как функцию, возвращающую Float, либо как процедуру с out параметром типа Float. Это возможно т. к., начиная с версии Ада 2012, функции могут иметь out и in out параметры. Несмотря на это, мы последовали традиционным путем и записали Pop как процедуру. По стилю вызовы Pop и Push будут единообразны, и тот факт, что вызов Pop имеет побочный эффект, будет более очевиден.
Тело пакета может выглядеть следующим образом:
package body Stacks is
procedure Clear (S : out Stack) is
begin
S.Top := 0;
end Clear;
procedure Push (S : in out Stack; X : in Float) is
begin
S.Top := S.Top + 1;
S.A (S.Top) := X;
end Push;
-- процедура Pop аналогично
end Stacks;
Теперь клиент может определить, сколько угодно стеков и работать с ними независимо:
with Stacks; use Stacks;
procedure Main is
This_Stack : Stack;
That_Stack : Stack;
begin
Clear (This_Stack); Clear (That_Stack);
Push (This_Stack, 37.4);
...
end Main;
Подробная информация о типе Stack дается в приватной части пакета и, хотя она видима читателю, прямой доступ к ней из кода клиента отсутствует. Таким образом, спецификация логически разделяется на две части — видимую (все что перед private) и приватную.
Изменения приватной части не приводят к необходимости исправлять исходный код клиента, однако модуль клиента должен быть перекомпилирован, поскольку его объектный код может измениться, хотя исходный текст и останется тем же.
Все необходимые перекомпиляции контролируются системой сборки и по желанию выполняются автоматически. Следует подчеркнуть, что это требования спецификации языка Ада, а не просто особенности конкретной реализации. Пользователю никогда не придется решать, нужно ли перекомпилировать модуль, таким образом, нет риска построить программу из несогласованных версий компилируемых модулей. Это большая проблема для языков, у которых нет точного механизма взаимодействия компилятора, системы сборки и редактора связей.
Также отметьте синтаксис указания режима параметров in, out и in out. Мы остановимся на них подробнее в главе «Безопасное создание объектов», где будет описана концепция потоков информации (information/data flow).
Контрактная модель настраиваемых модулей
Шаблоны — одна из важных возможностей таких языков программирования как C++ (а также недавно Java и C#). Им в Аде соответствуют настраиваемые модули (настраиваемые/обобщенные пакеты, generic packages). На самом деле, при создании шаблонов C++ были использованы идеи настраиваемых модулей Ады. Чтобы обеспечить безопасность типов данных, настраиваемые модули используют так называемую контрактную модель.
Мы можем расширить пример со стеком так, чтобы стало возможно определить стеки для произвольных типов и размеров (позже мы рассмотрим еще один способ сделать это). Рассмотрим следующий код
generic
Max : Integer;
type Item is private;
package Generic_Stacks is
type Stack is private;
procedure Clear (S : out Stack);
procedure Push (S : in out Stack; X : in Item);
procedure Pop (S : in out Stack; X : out Item);
private
type Vector is array (1 .. 100) of Item;
type Stack is record
A : Vector;
Top : Integer range 0 .. Max := 0;
end record;
end Generic_Stacks;
Тело к этому пакету можно получить из предыдущего примера, заменив Float на Item.
Настраиваемый пакет - это просто шаблон. Чтобы использовать его в программе, нужно сначала выполнить его настройку, предоставив два параметра — Max и Item. В результате настройки получается реальный пакет. К примеру, если мы хотим работать со стеками целых чисел с максимальным размером 50 элементов, мы напишем:
package Integer_Stacks is new Generic_Stacks
(Max => 50, Item => Integer);
Эта запись определяет пакет Integer_Stacks, который далее можно использовать как обычный. Суть контрактной модели в том, что если мы предоставляем параметры, отвечающие требованиям описания настраиваемого пакета, то при настройке мы гарантированно получим рабочий пакет, компилируемый без ошибок.
Другие языки не предоставляют этой привлекательной возможности. В C++, к примеру, некоторые несоответствия можно выявить только в момент сборки программы, а некоторые и вовсе могут остаться не обнаруженными, пока мы не запустим программу и не получим исключение.
Существуют разнообразные варианты настраиваемых параметров в языке Ада. Использованная ранее форма:
type Item is private;
позволяет использовать практически любой тип для настройки. Другая форма:
type Item is (<>);
обозначает любой скалярный тип. Сюда относятся целочисленные типы (такие как Integer и Long_Integer) и перечислимые типы (такие как Signal). Внутри настраиваемого модуля мы можем пользоваться всеми свойствами, общими для этих типов, и, несомненно, любой актуальный тип будет иметь эти свойства.
Контрактная модель настраиваемых модулей очень важна. Она позволяет вести разработку библиотек общего назначения легко и безопасно. Это достигается во многом благодаря тому, что пользователю нет необходимости разбираться с деталями реализации пакета, чтобы определить, что может пойти не так.
Дочерние модули
Общая архитектура системы (программы) на языке Ада может иметь иерархическую (древовидную) структуру, что облегчает сокрытие информации и упрощает модификацию. Дочерние модули могут быть общедоступными или приватными. Имея пакет с именем Parent мы можем определить общедоступный дочерний пакет следующим образом:
package Parent.Child is ...
а приватный как:
private package Parent.Child is ...
Оба варианта могут иметь тело и приватную часть, как обычно. Ключевая разница в том, что общедоступный дочерний модуль, по сути, расширяет спецификацию родителя (и таким образом видим всем клиентам), тогда как приватный модуль расширяет приватную часть и тело родителя (и таким образом не видим клиентам). У дочерних пакетов, в свою очередь, могут быть дочерние пакеты и так далее.
Среди правил, определяющих видимость имен, можно отметить следующее. Дочерний модуль не нуждается в спецификаторе контекста (with Parent), чтобы видеть объекты родителя. В тоже время, тело родителя может иметь спецификатор контекста для дочернего модуля, если нуждается в функциональности, предоставляемой им. Однако, поскольку спецификация родителя должна быть доступна к моменту компиляции дочернего модуля, спецификация родителя не может содержать «обычный» спецификатор контекста (with Child) для дочернего модуля. Мы обсудим это позже.
Согласно другому правилу, из видимой части приватного модуля видна приватная часть его родителя (в точности, как это происходит в теле пакета-родителя). Эта «дополнительная» видимость не нарушает родительскую инкапсуляцию, поскольку использовать приватные модули могут только те модули, которые и так видят приватную часть родителя. С другой стороны, в общедоступном модуле приватную часть родителя видно только из его приватной части и тела. Это обеспечивает инкапсуляцию данных родителя.
Особая форма спецификации контекста private with, которая была добавлена в Аде 2005, обеспечивает видимость перечисленных модулей в приватной части пакета. Это полезно, когда приватная часть общедоступного дочернего пакета нуждается в информации, предоставляемой приватным дочерним модулем. Допустим, у нас есть прикладной пакет App и два дочерних App.User_View и App.Secret_Details:
private package App.Secret_Details is
type Inner is ...
... -- различные операции для типа Inner
end App.Secret_Details;
private with App.Secret_Details;
package App.User_View is
type Outer is private;
... -- различные операции для типа Outer
-- тип Inner не видим здесь
private
type Outer is record
X : App.Secret_Details.Inner;
...
end record;
...
end App.User_View;
Обычный спецификатор контекста (with App.Secret_Details;) не допустим в User_View, поскольку это бы позволило клиенту увидеть информацию из пакета Secret_Details через видимую часть пакета User_View. Все попытки обойти правила видимости в Аде тщательно заблокированы.
Модульное тестирование
Одна из проблем, встречающаяся при тестировании кода, заключается в том, чтобы предотвратить влияние тестов на поведение тестируемого кода. Это напоминает известный феномен квантовой механики, когда сама попытка наблюдения за такими частицами, как электрон, влияет на состояние этой частицы.
Тщательно разрабатывая архитектуру программного обеспечения, мы стараемся скрыть детали реализации, сохранив стройную абстракцию, например, используя приватные типы. Но при тестировании системы мы хотим иметь возможность тщательно проанализировать поведение скрытых деталей реализаций.
В качестве простейшего примера, мы хотим знать значение Top одного из стеков, объявленных с помощью пакета Stacks (в котором находится приватный тип Stack). У нас нет готовых средств сделать это. Мы могли бы добавить функцию Size в пакет Stacks, но это потребует модификации пакета и перекомпиляции пакета и всего клиентского кода. Возникает опасность внести ошибку в пакет при добавлении этой функции, либо позже, при удалении тестирующего кода (и это будет гораздо хуже).
Дочерние модули позволяют решить эту задачу легко и безопасно. Мы можем написать следующее
package Stacks.Monitor is
function Size (S : Size) return Integer;
end Stacks.Monitor;
package body Stacks.Monitor is
function Size (S : Size) return Integer is
begin
return S.Top;
end Size;
end Stacks.Monitor;
Это возможно, так как тело дочернего модуля видит приватную часть родительского пакета. Теперь в тестах мы можем вызвать функцию Size как только нам понадобится. Когда мы убедимся, что наша программа корректна, мы удалим дочерний пакет целиком. Родительский пакет при этом не будет затронут.
Взаимозависимые типы
Эквивалент приватных типов есть во многих языках программирования, особенно в области ООП. По сути, операции, принадлежащие типу, это те, что объявлены рядом с типом в одном пакете. Для типа Stack такими операциями являются Clear, Push и Pop. Аналогичная конструкция в C++ выглядит так:
class Stack {
... /* детали реализации стека */
public:
void Clear();
void Push(float);
float Pop();
};
Подход C++ удобен тем, что использует один уровень при именовании — Stack, в то время, как в Аде мы используем два - имя пакета и имя типа, т.е. Stacks.Stack. Однако, этого, при желании, легко избежать, используя спецификатор использования — use Stacks. И, более того, появляется возможность выбора предпочитаемого стиля. Можно, например, назвать тип нейтрально — Object или Data, а затем ссылаться на него написав Stacks.Object или Stacks.Data.
С другой стороны, если в двух типах мы желаем для реализации использовать общую информацию, на языке Ада это может быть легко достигнуто:
package Twins is
type Dum is private;
type Dee is private;
...
private
... -- Общая информация для реализации
end Twins;
где в приватной части мы определим Dum и Dee так, что они будут иметь свободный взаимный доступ к данным друг друга.
В других языках это может быть не так просто. Например, в C++ нужно использовать довольно спорный механизм friend. Подход, используемый в Аде, предотвращает некорректное использование данных и раскрытие данных реализации и является при этом симметричным.
Следующий пример демонстрирует взаимную рекурсию. Допустим, мы исследуем схемы из линий и точек, при этом каждая точка лежит на пересечении трех линий, а каждая линия проходит через три точки. (Это пример на самом деле не случаен, две из фундаментальных теорем проективной геометрии оперируют такими структурами). Это легко реализовать в одном пакете, используя ссылочные типы:
package Points_And_Lines is
type Point is private;
type Line is private;
...
private
type Point is record
L, M, N : access Line;
end record;
type Line is record
P, Q, R : access Point;
end record;
end Points_And_Lines;
Если мы решим расположить каждый тип в своем пакете, это тоже возможно, но необходимо использовать специальную форму спецификатора контекста limited with, введенную в стандарте Ada 2005. (Два пакета не могут ссылаться друг на друга, используя обычный with, потому, что это вызовет циклическую зависимость между ними при инициализации). Мы напишем:
limited with Lines;
package Points is
type Point is private;
...
private
type Point is record
L, M, N : access Lines.Line;
end record;
end Points;
и аналогичный пакет для Lines. Данная форма спецификатора контекста обеспечивает видимость неполным описаниям типов из данного пакета. Грубо говоря, такая видимость пригодна лишь для использования в ссылочных типах.
Контрактное программирование
В примере со стеком, рассмотренном нами ранее, есть некоторые недочеты. Хотя он прекрасно иллюстрирует использование приватных типов для сокрытия деталей реализации, ничто в спецификации пакета не отражает того, что мы реализуем стек. Несмотря на то, что мы тщательно выбрали имена для операций со стеком, такие как Push, Pop и Clear, некто (по ошибке или злонамеренно) может использовать Push для извлечения элементов, а Pop — для их добавления. В целях повышения надежности и безопасности было бы полезно иметь механизм, который учитывает намерения автора в контексте семантики типа и подпрограмм, объявленных в пакете.
Такие средства были добавлены в стандарт Ада 2012. Они аналогичны предлагаемым в Eiffel средствам конрактного программирования. Воспользовавшись ими, программист указывает пред- и пост-условия для подпрограмм и инварианты приватных типов. Эти конструкции имеют форму логических условий. Специальные директивы компилятору включают проверку этих условий в момент исполнения. Чтобы привязать эти конструкции к соответствующему имени (пред/пост-условия к подпрограммам и инварианты к типам), используется новый синтаксис спецификации аспекта. Вкратце:
Пред-условие проверяется в точке вызова подпрограммы и отражает обязательства вызывающего;
Пост-условие проверяется при возврате из подпрограммы и отражает обязательства вызываемой подпрограммы;
Инвариант типа эквивалентен пост-условию для каждой подпрограммы типа, видимой вне пакета, поэтому проверяется при выходе из каждой такой подпрограммы. Инвариант отражает «глобальное» состояние программы после выхода из любой такой подпрограммы.
Представленная ниже версия пакета Stacks иллюстрирует все три концепции. Чтобы получить нетривиальный инвариант типа, мы ввели новое условие — стек не должен иметь повторяющиеся элементы.
package Stacks is
type Stack is private
with Type_Invariant => Is_Unduplicated (Stack);
function Is_Empty (S: Stack) return Boolean;
function Is_Full (S: Stack) return Boolean;
function Is_Unduplicated (S: Stack) return Boolean;
function Contains (S: Stack; X: Float) return Boolean;
-- Внимание! Из Contains(S,X) следует Is_Empty(S)=False
procedure Push (S: in out Stack; X: in Float)
with
Pre => not Contains(S,X) and not Is_Full(S),
Post => Contains(S,X);
procedure Pop (S: in out Stack; X: out Float)
with
Pre => not Is_Empty(S),
Post => not Contains(S,X) and not Is_Full (S);
procedure Clear (S: in out Stack)
with
Post => Is_Empty(S);
private
...
end Stacks;
Синтаксис спецификаций аспектов выглядит очевидным. Отсутствие пред-условия (как в Clear) эквивалентно пред-условию True.
Контракты (т. е. пред/пост-условия и инварианты) можно использовать по разному. В простейшем случае они уточняют намерения автора и выступают в роли формальной документации. Они также могут служить для генерации проверок соответствующих условий в момент исполнения. Директива Assertion_Policy управляет этим поведением. Она имеет форму
pragma Assertion_Policy(policy_identifier);
Когда policy_identifier равен Check, проверки генерируются, а если Ignore, то игнорируются. (Поведение по умолчанию, в отсутствии этой директивы, зависит от реализации компилятора.)
Третий способ использования контрактов способствует использованию формальных методов доказательства свойств программы, например, доказательство того, что код подпрограммы согласован с пред- и пост-условиями. Этот подход на примере языка SPARK мы обсудим в другой главе.
Стандарт Ada 2012 включает разнообразные конструкции, связанные с контрактным программированием, которые не попали в наш пример. Кванторные выражения (for all и for some) напоминают инструкции циклов. Функции-выражения позволяют поместить простейшую реализацию функций прямо в спецификацию пакета. Это выглядит логичным при задании пред/пост-условий, поскольку они являются частью интерфейса пакета. В Ada 2012 добавлены новые атрибуты: 'Old — позволяет в пост-условии сослаться на исходное значение формального параметра подпрограммы, а 'Result в пост-условии ссылается на результат, возвращаемый функцией. За более детальной информацией можно обратиться к стандарту языка или к разъяснениям стандарта (Rationale Ada 2012).
Следует отметить, что степень детализации условий контракта может значительно варьироваться. В нашем примере единственное требование к подпрограмме Push состоит в том, что элемент должен быть добавлен в стек. В то же время, семантика стека «последний вошел, первый вышел» более конкретна: элемент должен быть добавлен так, чтобы следующий вызов Pop его удалил. Аналогично, от Pop требуется, чтобы он вернул какой-то элемент. Если мы хотим быть более точными, необходимо указать, что этот элемент был добавлен последним. Подобные условия также можно написать, используя средства языка Ada 2012. Мы оставляем это читателю в качестве упражнения.