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


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


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


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


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


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


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


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


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


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



Контакти
 


Тлумачний словник
Авто
Автоматизація
Архітектура
Астрономія
Аудит
Біологія
Будівництво
Бухгалтерія
Винахідництво
Виробництво
Військова справа
Генетика
Географія
Геологія
Господарство
Держава
Дім
Екологія
Економетрика
Економіка
Електроніка
Журналістика та ЗМІ
Зв'язок
Іноземні мови
Інформатика
Історія
Комп'ютери
Креслення
Кулінарія
Культура
Лексикологія
Література
Логіка
Маркетинг
Математика
Машинобудування
Медицина
Менеджмент
Метали і Зварювання
Механіка
Мистецтво
Музика
Населення
Освіта
Охорона безпеки життя
Охорона Праці
Педагогіка
Політика
Право
Програмування
Промисловість
Психологія
Радіо
Регилия
Соціологія
Спорт
Стандартизація
Технології
Торгівля
Туризм
Фізика
Фізіологія
Філософія
Фінанси
Хімія
Юриспунденкция






Мова формальної специфікації – 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




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

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

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

 

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


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