• Гідрологія і Гідрометрія
• Господарське право
• Економіка будівництва
• Економіка природокористування
• Економічна теорія
• Земельне право
• Історія України
• Кримінально виконавче право
• Медична радіологія
• Методи аналізу
• Міжнародне приватне право
• Міжнародний маркетинг
• Основи екології
• Предмет Політологія
• Соціальне страхування
• Технічні засоби організації дорожнього руху
• Товарознавство продовольчих товарів

Мова формальної специфікації – RAISE

Мова RAISE і RSL–специфікація (RAISE Specification Language) були розроблені в 80-роках як результат попереднього дослідження формальних методів верифікації програм і їх поповнення новими можливостями стосовно їх доказу. Метод містить нотації, техніку і інструменти для формального опису ( RSL, С++ і Паскаль) програм і доказу їх правильності.

До складу мови RSL входять абстрактні параметричні типи даних (специфікації, алгебри) і конкретні типи даних (модельно–орієнтовані), підтипи, операції для завдання послідовних і паралельних програм. Тобто ця мова надає аплікативний і імперативний стиль специфікації абстрактних програм, а також формальне конструювання окремих програм в інших мовах програмування і апарат доказу їх правильності. Синтаксис цієї мови близький до синтаксису мов С++ і Паскаль.

У мові RSL є абстрактні типи даних і конструктори складних типів даних, такі як добуток (product), множини (sets), списки (list), відображення (map), записи (record) і т.п.

Добуток типів – це впорядкована скінчена послідовність типів Т1, Т2 ., Тn добутку (product) Т1 ´ Т2 ., ´ Тn .

Кількість компонентів добутку d – це size (d) = id Ñ (null (couter inc(counter))).

Конструктор добутку d1 і d2 будує добуток d1 ´ d2 і значення типу product (Т1´ Т, ´ Тn) – тобто

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

де значення value i має тип Т_i, а результуюче значення – тип добутку Т₁ ´Т₂ ´, …, ´ Т_n має значення Ñ (value n n).

Списки типів – це послідовність значень одного типу list Т, можуть бути кінцевим списком типів Тk і некінцевим списком типів Tn. У якості структури даних типу список може бути бінарне дерево, в якому є голова (head), син ( tail), який слідує за ним у списку, і хвіст. До операцій списку відноситься операція hd – узяття першого елементу списку, тобто голови, і операція tl – узяття хвоста – решти елементів (як у мові VDM).

Функція Caddr (I) = L Þ tail Þ tail Þ Head вибирає із списку I елемент та індекс голови елементу, кількість елементів у списку і ін.

Відображення – це структура (map), яка ставить у відповідність значенням одного типу значення іншого типу. Разом з тим відображення – це бінарне відношення декартові добутку двох множин як сукупності двокомпонентних пар, в яких перший компонент – arg містить елементи аргументів відображення, а другий компонент – res містить відповідні елементи значень цього відображення.

Операції над відображеннями такі: накладення, об'єднання, композиція, зріз, композиція відображень (m₁, m₂).

Запис – це сукупність іменованих полів даних. Цей тип відповідає типу recordу мові Паскаль і struct у мові С++. У мові RAISE для запису визначено два конструктори – record, shurt record.

Об'єднання– це конструктор union,що забезпечує об'єднання типів, наприклад,

typeid = id₁, id₂,., idn і тип id , який одержує одне із значень у списку елементів.

Конструктор типу – це тип виду type id = id_from_ id1 (id_to_ id1: id1.

Таким чином, мови VDM і RAISE слугують для математичного опису програм і конструювання структур даних як специфікацій, що використовуються при доказі програм.

Читайте також:

1. Кількісна характеристика товару подається у специфікації, технічній документації, пакувальному листі.
2. Концепторна мова специфікації
3. Мова специфікації об’єктів 2 типу РПС
4. Мова формальної специфікацій – VDM
5. Мови специфікації програм –VDM, RAISE, Concept
6. Наслідки неформальної передачі інформації
7. Паспорт неформальної підліткової групи
8. Поняття організації. Сутність і основні риси формальної організації
9. Поняття та означення формальної системи знань
10. Специфікації фізичного середовища стандарту 802.3z

Переглядів: 898