Студопедия
Новини освіти і науки:
МАРК РЕГНЕРУС ДОСЛІДЖЕННЯ: Наскільки відрізняються діти, які виросли в одностатевих союзах


РЕЗОЛЮЦІЯ: Громадського обговорення навчальної програми статевого виховання


ЧОМУ ФОНД ОЛЕНИ ПІНЧУК І МОЗ УКРАЇНИ ПРОПАГУЮТЬ "СЕКСУАЛЬНІ УРОКИ"


ЕКЗИСТЕНЦІЙНО-ПСИХОЛОГІЧНІ ОСНОВИ ПОРУШЕННЯ СТАТЕВОЇ ІДЕНТИЧНОСТІ ПІДЛІТКІВ


Батьківський, громадянський рух в Україні закликає МОН зупинити тотальну сексуалізацію дітей і підлітків


Відкрите звернення Міністру освіти й науки України - Гриневич Лілії Михайлівні


Представництво українського жіноцтва в ООН: низький рівень культури спілкування в соціальних мережах


Гендерна антидискримінаційна експертиза може зробити нас моральними рабами


ЛІВИЙ МАРКСИЗМ У НОВИХ ПІДРУЧНИКАХ ДЛЯ ШКОЛЯРІВ


ВІДКРИТА ЗАЯВА на підтримку позиції Ганни Турчинової та права кожної людини на свободу думки, світогляду та вираження поглядів



Мова формальної специфікації – 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, а результуюче значення – тип добутку Т1 ´Т2 ´, …, ´ Тn має значення Ñ (value n n).

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

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

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

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

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

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

typeid = id1, id2,., 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




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

<== попередня сторінка | наступна сторінка ==>
Мова формальної специфікацій – VDM | Концепторна мова специфікації

Не знайшли потрібну інформацію? Скористайтесь пошуком google:

  

© studopedia.com.ua При використанні або копіюванні матеріалів пряме посилання на сайт обов'язкове.


Генерація сторінки за: 0.01 сек.