Методы и средства инженерии программного обеспечения


Формальные методы - часть 3


описанных в RSL и ЯП (С++ и Паскаль).

Язык RSL содержит абстрактные параметрические типы данных (алгебраические спецификации)  и конкретные типы данных  (модельно–ориентированные), подтипы,  операции для задания последовательных и  параллельных программ, предоставляет аппликативный и императивный стиль спецификации абстрактных программ, а также  формальное конструирование программ в других ЯП  и доказательства их правильности. Синтаксис этого языка близок  к синтаксису  языков С++ и Паскаль.

В  RSL–языке имеются предопределенные абстрактные типы данных и конструкторы сложных типов данных, такие как произведение (product), множества (sets), списки (list), отображения (map), записи (record) и т.п. Далее рассмотрим, для примера,   некоторые конструкторы сложных типов данных.

1. Произведение типов – это упорядоченная конечная последовательность типов   Т1, Т2 , …, Тn   произведения  (product)  Т1 ´ Т2 ´, …, ´ Тn  .  Представитель типа имеет вид (v1, v2 , …, vn ), где каждое  vi    есть значением типа   Тi.  Компонент произведения можно   получить get и переслать set, т.е.

            get component  (i, d) = getvalue (i, d),

            set  component  (d, i, val)  = d ÞÑ  (I ® val).

Количество компонентов  произведения d  находится таким образом:

            size (d) = id  Ñ (null (couter  inc(counter))).

Конструктор произведения d1 и d2  строит произведение d1 ´ d2   вида

         product  (d1 , d2  ) =  id Ñ (size (d1)  Þ couter 1)  Ñ (null (couter 2) inc couter 2))).

Для каждого конкретного типа product (Т1 ´Т2

´, …, ´ Тn) можно построить конструктор значения этого типа из отдельных компонентов произведения  таким образом:

            make product (value 1, …, value n) = (value i Þ 1)  Ñ… Ñ  (value n Þ n),

где каждое значение value i  имеет тип Тi  ,  а результирующее значение – тип произведения Т1 ´Т2 ´, …, ´ Тn .




- Начало -  - Назад -  - Вперед -