Формальные методы - часть 5
apply to composition (m1, m2, elem) =
(ld Ñ (image (elem, m1) Þ s) restrict (m2, s) Þ map
(ld Ñ (map getname elem Þ name)) getvalue (name, map).
При этом используются функции:
Apply (m, elem) = image (elem, m) elem Þ,
Apply (m, elem) = getvalue (elem, m) elem Þ.
4. Запись – это совокупность именованных полей. Этот тип соответствует типу record в языке Паскаль и struct в языке С++. В языке RAISE определено два конструктора типа, record, shurt record, которые описываются в виде – type record id =
type mk_id (short _record id ) ::=
destr_id1 : type_expr1 « recon_id
. . .
destr_idn : type_exprn « recon_id.
Идентификатор mk_id является конструктором типа record, для которого даны деструкторы destr_idn , как функции получения значения компонентов записи.
5. Объединение – это конструктор Union, обеспечивающий объединение типов
type id = id1 , id2 ,…, idn
при котором тип id получает одно из значений в списке элементов.
Конструктор этого типа имеет вид:
type id = id_from_ id1 (id_to_ id1: id1) ½… ½ id_from_ idn (id_to_ idn: idn)/
Операции над самим типом не определены в языке RAISE.
Рассмотренные формальные структуры данных языка RAISE позволяет математически описывать и конструировать новые структуры данных в проектируемых программах. Их проще проверять на правильность методами верификации.