ГОСТ Р HCO/HL7 27951—2016
антного утверждения заключено в фигурные скобки. Оно содержит список высказываний, которые все должны
быть истинными.
invariant(BLх}
where x.nonNull {
х.
ana(true}.equal(*};
j
;
Инвариантное утверждение имеет семантику логического предиката с квантором общности («для всех»).
Приведенное выше инвариантное утверждение может быть прочитано на естественном языке следующим
образом: «Для всех значений х типа Boolean, где х не является пустым, справедливо высказывание «х AND true
равно х». Все свойства должны быть именованными, чтобы высказывания можно было читать как предложения на
естественном языке’).
Если для инвариантного утверждения аргументы не требуются, то список аргументов указывать в нем не
надо.
invariant
1
true.not.equal(taise};
£alse.not.equal(true
} ;
1;
В.1.9.2.1 Выражение высказывания
Высказывания, включенные в инвариантные утверждения, представляют собой выражения, аргументами
которых являются семантические свойства определяемых типов данных. Выражение высказывания должно иметь
значение типа Boolean {«true» или «false»)2’. Никакие примитивные типы данных или операции не существуют до
определения типов данных. Единственными предопределенными свойствами языка выражений высказываний
являются3);
- строки символов, представляющие словесные выражения языка определения типов данных:
- понятие справедливости высказывания ((rue) или его ложности (false)4,
- инвариантное утверждение: invariant...) where ...
- выражение квантора общности в форме forall (...) where ... {...}; является синонимом инвариантного утверж
дения;
- выражения квантора существования в форме exists (...) where ... {...};
- явная конъюнкция (логический оператор AND) между утверждениями: утверждение^; утверждение_2; ...
утверждение^, разделенными точками с запятой:
- переменные и объявления в списке аргументов инвариантного утверждения;
- ссылка на свойство с помощью точки: x.property;
- явное и неявное преобразование типов: (Т)х;
’) Синтаксис и семантика инвариантного учреждения похожи на конструкцию «inv» в языке OCL. Однако
этот язык не используется в настоящей спецификации по следующим причинам: (1) стиль синтаксиса языка OCL
напоминает Smalltalk, отличающихся от стиля определения типов данных в языках C++.‘Java; (2) в языке OCL
предусмотрено много примитивных конструкцию и типов данных, чего настоящий стандарт старается по возмож
ности избежать; (3) богатство примитивных конструкций в языке OCL является одной из причин его сложности, не
требуемой в настоящей спецификации.
2>Эта конструкция в определенном отношении является циклической; она исходит из существования типа
данных Boolean, хотя этот тип данных сам определен таким же образом, как и другие типы данных. Кроме того,
поскольку данный язык определения типов данных представлен в виде строк символов, понятие строки симво лов
должно существовать до определения строкового типа данных character string. Таким образом, эти два типа,
character string и Boolean, являются особыми, но на первый взгляд они определены аналогично другим типам дан
ных. Поскольку не предполагается, что данная спецификация типов данных будет реализована, такая цикличность не
представляет собой особую проблему. Даже если бы этот язык предполагалось реализовать, можно было бы
использовать технологию «самозагрузки», которая вполне обычна, к примеру, в компиляторах, которые компили
руют сами себя.
3* Большинство этих синтаксических свойств навеяно языком JAVA: использование списков аргументов,
фигурные скобки для окаймления блоков, точка с запятой для завершения утверждения и точка для ссылки на
свойства значения. Удвоенное двоеточиеиспользуемое в языках C++ и IDL для различения ссылки на члена и
ссылки на значение, здесь не используется (как и в языке Java). В отличив от языка Java и ближе к языкам C++ и IDL
каждое утверждение завершается точкой с запятой, в том числе декларации типа. Неявное преобразование типов
также позаимствовано у языка C++.
292