4.1 Формальные спецификации, написанные на EXPRESS
4.1.1 Лексический язык
Формальная спецификация, написанная на EXPRESS, должна быть согласована с заданным уровнем, как указано ниже. Формальная спецификация согласована с заданным уровнем, когда все проверки, установленные для этого уровня и всех нижних уровней, удовлетворены для этой спецификации.
Уровни проверки
Уровень 1: проверка ссылок. Данный уровень состоит из проверки формальной спецификации, гарантирующей ее синтаксическую и ссылочную корректность. Формальная спецификация синтаксически корректна, если она соответствует синтаксису, полученному расширением первичных синтаксических правил (синтаксиса), установленных в приложении А. Формальная спецификация корректна в отношении ссылок, если все ссылки на каждый элемент описания языка EXPRESS соответствуют области применения и правилам видимости, установленным в разделах 10 и 11.
Уровень 2: проверка типов. Данный уровень состоит из проверки формальной спецификации, гарантирующей ее соответствие следующему:
- выражения должны удовлетворять правилам, установленным в разделе 12;
- присваивания должны удовлетворять правилам, установленным в 13.3;
- объявления инверсных атрибутов должны удовлетворять правилам, установленным в 9.2.1.3;
- переобъявления атрибутов должны удовлетворять правилам, установленным в 9.2.3.4.
Уровень 3: проверка значения. Данный уровень состоит из проверки формальной спецификации, гарантирующей ее соответствие утверждениям вида "А должно быть больше В", как установлено в разделах 7-16. Проверка справедлива для тех положений, в которых А и В могут быть выражены литералами и/или константами.
Уровень 4: полная проверка. Данный уровень состоит из проверки формальной спецификации, гарантирующей ее соответствие всем формулировкам требований, установленным в настоящем стандарте.
Пример 1 - В настоящем стандарте установлено, что функция должна иметь оператор возврата ("return") для каждой из возможных ветвей, по которым может пойти процесс после вызова данной функции. Это должно быть проверено.
4.1.2 Графическая форма
Формальная спецификация, написанная на EXPRESS-G, должна быть согласована с заданным уровнем, как указано ниже. Формальная спецификация согласована с заданным уровнем, когда все проверки, установленные для этого уровня и всех нижних уровней, удовлетворены для этой спецификации.
Уровни проверки
Уровень 1: проверка символов и области применения. Данный уровень состоит из проверки формальной спецификации, гарантирующей ее соответствие как требованиям к уровню объекта, так и требованиям к уровню схемы, как определено в D.5 и D.6. Это охватывает проверку того, что в формальной спецификации символы используются в соответствии с D.2-D.4. Формальная спецификация также должна быть проверена на соответствие страничных ссылок и переобъявленных атрибутов требованиям D.4.1 и D.5.5.
Уровень 2: полная проверка. Данный уровень состоит из проверки формальной спецификации для установления тех мест, которые не соответствуют требованиям к полному уровню объекта или полному уровню схемы, определенным в приложении D, и требованиям, установленным в разделах 7-16.
4.2 Реализации EXPRESS
4.2.1 Синтаксический анализатор языка EXPRESS
Реализация синтаксического анализатора языка EXPRESS должна выполнять синтаксический разбор любой формальной спецификации, написанной на EXPRESS, в соответствии с ограничениями, установленными в приложении Е и связанными с этой реализацией. Синтаксический анализатор языка EXPRESS будет считаться соответствующим конкретному уровню проверки (как установлено в 4.1.1), если он может применять все проверки, требуемые для данного уровня (и любых нижележащих уровней), к формальной спецификации, написанной на EXPRESS.
Разработчик синтаксического анализатора языка EXPRESS должен установить любые ограничения, которые реализация накладывает на число и длину идентификаторов, на диапазон обрабатываемых чисел и на максимальную точность действительных чисел. Такие ограничения должны быть документально оформлены в виде, установленном в приложении Е, с целью проведения аттестационного тестирования.
4.2.2 Средство графического редактирования
Реализация редактора EXPRESS-G должна обеспечивать возможности создания и отображения формальных спецификаций на EXPRESS-G, в соответствии с ограничениями, установленными в приложении Е и связанными с этой реализацией. Редактор EXPRESS-G будет считаться соответствующим конкретному уровню проверки, если он может создавать и отображать формальные спецификации на EXPRESS-G, которые соответствуют указанному уровню проверки (и любому нижележащему уровню).
Разработчик редактора EXPRESS-G должен установить любые ограничения, которые реализация накладывает на число и длину идентификаторов, на число доступных символов на страницу модели и на максимальное число страниц. Такие ограничения должны быть документально оформлены в виде, установленном в приложении Е, с целью проведения аттестационного тестирования.