МАРК РЕГНЕРУС ДОСЛІДЖЕННЯ: Наскільки відрізняються діти, які виросли в одностатевих союзах
РЕЗОЛЮЦІЯ: Громадського обговорення навчальної програми статевого виховання ЧОМУ ФОНД ОЛЕНИ ПІНЧУК І МОЗ УКРАЇНИ ПРОПАГУЮТЬ "СЕКСУАЛЬНІ УРОКИ" ЕКЗИСТЕНЦІЙНО-ПСИХОЛОГІЧНІ ОСНОВИ ПОРУШЕННЯ СТАТЕВОЇ ІДЕНТИЧНОСТІ ПІДЛІТКІВ Батьківський, громадянський рух в Україні закликає МОН зупинити тотальну сексуалізацію дітей і підлітків Відкрите звернення Міністру освіти й науки України - Гриневич Лілії Михайлівні Представництво українського жіноцтва в ООН: низький рівень культури спілкування в соціальних мережах Гендерна антидискримінаційна експертиза може зробити нас моральними рабами ЛІВИЙ МАРКСИЗМ У НОВИХ ПІДРУЧНИКАХ ДЛЯ ШКОЛЯРІВ ВІДКРИТА ЗАЯВА на підтримку позиції Ганни Турчинової та права кожної людини на свободу думки, світогляду та вираження поглядів Контакти
Тлумачний словник |
|
|||||||
Мова формальної специфікації – 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 слугують для математичного опису програм і конструювання структур даних як специфікацій, що використовуються при доказі програм. Читайте також:
|
||||||||
|