Формальные методы - часть 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 позволяет математически описывать и конструировать новые структуры данных в проектируемых программах.  Их проще проверять на правильность  методами верификации.