ГОСТ Р ИСО 10303-11-2009 Системы автоматизации производства и их интеграция. Представление данных об изделии и обмен этими данными. Часть 11. Методы описания. Справочное руководство по языку EXPRESS

     4.1.1 Лексический язык

Формальная спецификация, написанная на языке EXPRESS, должна быть согласована с заданным уровнем, как определено ниже. Формальная спецификация считается согласованной с заданным уровнем, если все проверки, установленные для данного уровня и всех более низких уровней, верифицированы для данной спецификации.

Уровни проверки

Уровень 1 - проверка ссылок. Данный уровень состоит из проверки формальной спецификации для подтверждения ее синтаксической и ссылочной корректности. Формальная спецификация синтаксически корректна, если она соответствует синтаксису, сформированному посредством расширения основного синтаксического правила (syntax), установленного в приложении А. Формальная спецификация корректна в отношении ссылок, если все ссылки на элементы языка EXPRESS соответствуют области применения и правилам видимости, установленным в разделах 10 и 11.

Уровень 2 - проверка типов. Данный уровень включает в себя проверку формальной спецификации для подтверждения ее соответствия следующим требованиям:

- выражения должны удовлетворять правилам, установленным в разделе 12;

- присваивания должны удовлетворять правилам, установленным в 13.3;

- объявления инверсных атрибутов должны удовлетворять правилам, установленным в 9.2.1.3;

- повторные объявления атрибутов должны удовлетворять правилам, установленным в 9.2.3.4.

Уровень 3 - проверка значений. Данный уровень состоит из проверки формальной спецификации для подтверждения ее соответствия утверждениям типа "А должно быть больше В", установленным в разделах 7-16. Данная проверка ограничена случаями, когда значения А и В могут быть выражены литералами и/или константами.

Уровень 4 - полная проверка. Данный уровень включает в себя проверку формальной спецификации для подтверждения ее соответствия формулировкам требований, установленных в настоящем стандарте.

Пример - В настоящем стандарте установлено, что функции должны содержать оператор возврата для каждой из возможных ветвей, по которым может пойти процесс при вызове данной функции, что и должно быть проверено.