Руководство по Ada (Ada 2022)
H.4 Ограничения высокой надёжности
В этом подпункте определены ограничения, которые могут использоваться с директивой Restrictions (см. 13.12); они облегчают демонстрацию корректности программы, позволяя использовать настроенные версии среды выполнения.
Статическая семантика
Этот абзац был удалён.
Следующие ограничение_идентификаторы определены языком:
Ограничения, связанные с задачами:
No_Protected_Types
Нет объявлений защищённых типов или защищённых объектов.
Ограничения, связанные с управлением памятью:
No_Allocators
Нет случаев использования аллокатора.
No_Local_Allocators
Аллокаторы запрещены в подпрограммах, обобщённых подпрограммах, задачах и телах входов.
No_Anonymous_Allocators
Нет аллокаторов анонимных типов доступа.
No_Coextensions
Нет корасширений. См. 3.10.2.
No_Access_Parameter_Allocators
Этот абзац был удалён.
Immediate_Reclamation
За исключением памяти, занимаемой объектами, созданными аллокатором и не освобождёнными с помощью неявного освобождения, любая выделенная во время выполнения память для объекта немедленно освобождается, когда объект больше не существует.
Ограничения, связанные с исключениями:
No_Exceptions
Оператор_вызова_исключения и обработчик_исключений не допускаются. Не генерируются никакие определённые языком проверки во время выполнения; однако, допускается проверка во время выполнения, выполняемая автоматически аппаратурой. Вызываемый объект, связанный с процедурным_итератором (см. 5.5.3), считается не допускающим выход, независимо от значения аспекта Allows_Exit.
Другие ограничения:
No_Floating_Point
Не допускается использование предопределённых типов и операций с плавающей точкой, а также объявление новых типов с плавающей точкой.
No_Fixed_Point
Не допускается использование предопределённых типов и операций с фиксированной точкой, а также объявление новых типов с фиксированной точкой.
Этот абзац был удалён.
No_Access_Subprograms
Не допускается объявление типов доступа к подпрограммам.
No_Unchecked_Access
Атрибут Unchecked_Access не допускается.
No_Dispatch
Не допускаются обращения к T'Class для любого (меченного) подтипа T.
No_IO
Не допускается семантическая зависимость от каких-либо из библиотечных единиц Sequential_IO, Direct_IO, Text_IO, Wide_Text_IO, Wide_Wide_Text_IO, Stream_IO или Directories.
No_Delay
Оператор_задержки и семантическая зависимость от пакета Calendar не допускаются.
No_Recursion
Во время выполнения подпрограммы не вызывается та же подпрограмма.
No_Reentrancy
Во время выполнения подпрограммы задачей, никакая другая задача не вызывает ту же самую подпрограмму.
No_Unspecified_Globals
Ни один библиотечный элемент не должен иметь аспект Global типа Unspecified, ни явно, ни по умолчанию. Ни один библиотечный элемент не должен иметь аспект Global'Class типа Unspecified, явно или по умолчанию, если он используется в вызове диспетчеризации.
No_Hidden_Indirect_Globals
В контексте, где соответствующий глобальный аспект не является Unspecified или in out all, любое выполнение в таком контексте не делает следующее:
Обновлять (или возвращать запись на доступ к) переменную, доступную через последовательность нуля или более обращений к значениям доступа к объекту из параметра видимого типа доступа к константе, из части формального параметра типа без доступа с режимом in (после любого переопределения – см. H.7) или из глобальной переменной с режимом in или не из набора глобальных переменных, за исключением случая, когда начальное обращение является частью формального параметра или глобальной переменной, которая явно является типом доступа к переменной;
Читать (или возвращать чтение на доступ к) переменную, доступную через последовательность нуля или более обращений к значениям доступа к объекту из глобальной переменной, которая не входит в соответствующий набор глобальных переменных, за исключением случая, когда начальное обращение является частью формального параметра или глобальной переменной, которая явно является типом доступа к объекту.
Для целей вышеупомянутых правил:
часть объекта видимо является типом доступа, если тип объекта объявлен непосредственно в видимой части спецификации пакета, и в момент объявления типа часть видима и является типом доступа;
функция возвращает запись на доступ к V, если она возвращает результат с частью, которая видимо является типом доступа к переменной, обозначающей V; аналогично, функция возвращает чтение на доступ к V, если она возвращает результат с частью, которая видимо является типом доступа к константе, обозначающей V;
если соответствующий набор глобальных переменных включает имя пакета, и коллекция некоторого специфичного для пула типа доступа (см. 7.6.1) неявно объявлена в части области объявления пакета, включённого в набор глобальных переменных, то все объекты, выделенные из этой коллекции, считаются включёнными в набор глобальных переменных.
Последствия нарушения ограничения No_Hidden_Indirect_Globals определяются реализацией. Любые аспекты или другие средства для определения таких нарушений до или во время выполнения определяются реализацией.
Динамическая семантика
Следующий ограничение_параметр_идентификатор определён языком:
Max_Image_Length
Указывает максимальную длину результата атрибутов Image, Wide_Image или Wide_Wide_Image. Нарушение этого ограничения приводит к возникновению исключения Program_Error в момент вызова атрибута изображения.
Требования к реализации
Реализация этого приложения должна поддерживать:
- ограничения, определённые в этом подпункте; и
- следующие ограничения, определённые в D.7: No_Task_Hierarchy, No_Abort_Statement, No_Implicit_Heap_Allocation, No_Standard_Allocators_After_Elaboration; и
- директиву Profile(Ravenscar); и
- следующие использования ограничение_параметр_идентификаторов, определённые в D.7, которые проверяются перед выполнением программы:
Max_Task_Entries => 0,
Max_Asynchronous_Select_Nesting => 0, и
Max_Tasks => 0.
Если ограничение Max_Image_Length относится к любому модулю компиляции в разделе, то для любого подтипа S атрибуты S'Image, S'Wide_Image и S'Wide_Wide_Image должны быть реализованы в этом разделе без динамического выделения.
Если реализация поддерживает директиву Restrictions для конкретного аргумента, то за исключением ограничений No_Access_Subprograms, No_Unchecked_Access, No_Specification_of_Aspect, No_Use_of_Attribute, No_Use_of_Pragma, No_Dependence => Ada.Unchecked_Conversion и No_Dependence => Ada.Unchecked_Deallocation, соответствующее ограничение относится к среде выполнения.
Требования к документации
Если указана директива Restrictions(No_Exceptions), реализация должна документировать эффекты всех конструкций, где проверки, определённые языком, всё ещё выполняются автоматически (например, проверка переполнения, выполняемая процессором).
Ошибочное выполнение
Выполнение программы является ошибочным, если директива Restrictions(No_Exceptions) была указана, и возникают условия, при которых сгенерированная языковая проверка во время выполнения потерпела бы неудачу.
END_OF_DOCUMENT_MARKER
Выполнение программы ошибочно, если указана директива Restrictions(No_Recursion), и подпрограмма вызывается в ходе собственного выполнения, или если указана директива Restrictions(No_Reentrancy), и во время выполнения подпрограммы задачей другая задача вызывает ту же подпрограмму.
ПРИМЕЧАНИЕ Использование параметра ограничения restriction_parameter_идентификатор No_Dependence, определённого в 13.12.1: No_Dependence => Ada.Unchecked_Deallocation и No_Dependence => Ada.Unchecked_Conversion могут быть подходящими для систем высокой надёжности. Другие применения No_Dependence также могут быть подходящими для систем высокой надёжности.
