:: ECONOMY :: ВЕРИФІКАЦІЯ КОМПОЗИЦІЙНИХ СХЕМ У МАКРОМОДУЛЬНОМУ ПРОГРАМУВАННІ :: ECONOMY :: ВЕРИФІКАЦІЯ КОМПОЗИЦІЙНИХ СХЕМ У МАКРОМОДУЛЬНОМУ ПРОГРАМУВАННІ
:: ECONOMY :: ВЕРИФІКАЦІЯ КОМПОЗИЦІЙНИХ СХЕМ У МАКРОМОДУЛЬНОМУ ПРОГРАМУВАННІ
 
UA  RU  EN
         

Світ наукових досліджень. Випуск 29

Термін подання матеріалів

23 квітня 2024

До початку конференції залишилось днів 26



  Головна
Нові вимоги до публікацій результатів кандидатських та докторських дисертацій
Редакційна колегія. ГО «Наукова спільнота»
Договір про співробітництво з Wyzsza Szkola Zarzadzania i Administracji w Opolu
Календар конференцій
Архів
  Наукові конференції
 
 Лінки
 Форум
Наукові конференції
Наукова спільнота - інтернет конференції
Світ наукових досліджень www.economy-confer.com.ua

 Голосування 
З яких джерел Ви дізнались про нашу конференцію:

соціальні мережі;
інформування електронною поштою;
пошукові інтернет-системи (Google, Yahoo, Meta, Yandex);
інтернет-каталоги конференцій (science-community.org, konferencii.ru, vsenauki.ru, інші);
наукові підрозділи ВУЗів;
порекомендували знайомі.
з СМС повідомлення на мобільний телефон.


Результати голосувань Докладніше

 Наша кнопка
www.economy-confer.com.ua - Економічні наукові інтернет-конференції

 Лічильники
Українська рейтингова система

ВЕРИФІКАЦІЯ КОМПОЗИЦІЙНИХ СХЕМ У МАКРОМОДУЛЬНОМУ ПРОГРАМУВАННІ

 
22.08.2021 16:34
Автор: Буяк Леся Михайлівна, доктор економічних наук, професор, кафедра економічної кібернетики та інформатики, Західноукраїнський національний університет; Мушак Андрій Ярославович, кандидат технічних наук, доцент, кафедра економічної кібернетики та інформатики, Західноукраїнський національний університет; Данилюк Ірина Вадимівна, кандидат економічних наук, доцент, кафедра економічної кібернетики та інформатики, Західноукраїнський національний університет
[Інформаційні системи і технології]

Макромодульний підхід у програмуванні включає питання, які стосуються семантичного аспекту програмування загалом [1] та програмуванню спеціально розробленою мовою зокрема. Розглянемо окремі з них. 

Проаналізуємо оператор цієї мови, який задається синтаксичною формулою вигляду:

do <послідовність операторів>

while(<логічна формула>)

Означення. Логічна формула — це ланцюжок символів, які зображаються предикатом <логічна формула> в елементарній формальній системі з аксіомами:

1. <функціональний символ> +|-|*|/;

2. <предикатний символ> <|>|=;

3. <константа>x → <терм>x

4. <проблемна змінна>x → <терм>x

5. <функціональний символ>x → <терм>y → <рм>z<терм>yxz;

6. <предикатний символ>x → <терм>y → <терм>z<атом>yxz;

7. <атом>x; → <логічна формула>x;

8. <логічна формула>x → <логічна формула> y → <логічна формула>-x|x&y|x y.

Принципове питання полягає у тому, чи є довільна логічна формула загальнозначимою, чи ні. У першому випадку розглянута вище мовна конструкція призводить до „зациклювання” композиційної схеми, яка її містить. У по-іншому цикл завершується через скінченну кількість кроків.

Відомо [2], що не існує алгоритму який дозволяє розпізнати загальнозначимість довільної логічної формули. Це пов’язано з існуванням нескінченної кількості можливих інтерпретацій логічних формул. Але деякі окремі результати в цьому напрямку були одержані. Основна їх ідея полягає у тому, щоб спростити перевірку загальнозначимості формул. Це було зроблено шляхом побудови спеціальної області інтерпретації логічної формули — ербранівського базису. Він означується так:

1. Для будь-якої індивідної константи a, яка входить в логічну формулу G, покладемо a є H0. Якщо G не містить індивідних констант, то вважатимемо H0 = (c).

2. Для кожного n-місного функціонального символа f та індивідних констант a1,...,an є H0 вважатимемо f(a1,...,an) є Ha.

3. Для кожного n-місного функціонального символа f та термів g(a1,...,an),...,h(b1,...,bn) є H1 вважатимемо f (g(a1,...,an),...,h(b1,...,bn)) є Ha.

4. І так далі.

Тоді ербранівський базис H логічної формули G є об’єднанням H=H0ᴗH1ᴗ... . Зрозуміло, що при відсутності функціональних та індивідних констант ербранівський базис зводиться до множини H={c}.

Зрозуміло, що для перевірки незагальнозначимості (виконання) довільної логічної формули достатньо спростувати її на ербранівській області.

Означення. Основним прикладом диз’юнкта множини диз’юнктів S називатимемо терм, отриманий підстановкою в нього елементів ербранівського базису замість змінних.

Алгоритм доведення незагальнозначимості довільної логічної формули ґрунтується на наступній теоремі.

Теорема. Множина диз’юнктів S незагальнозначима тоді і тільки тоді, коли існує невиконувана множина S` основних прикладів диз’юнктів S.

Нехай існує скінченна невиконувана множина S` основних прикладів диз’юнктів S. Це значить, що в деякій інтерпретації I скінченна кількість диз’юнктів з S спростовується. Тому і S спростовується. Тобто S — незагальнозначима.

Процедура спростування полягає у наступному.

1. Перетворимо логічну формулу в КНФ.

2. Визначимо ербранівський базис множини диз’юнктів по рівням H0,H1,... .

3. i=0 .

4. Породжуємо множину основних прикладів диз’юнктів Si шляхом заміни змінних в S константами з Hi.

5. Якщо Si невиконувана, незагальнозначимість S встановлена.

6. i=i+1 . Перехід на 4.

Цей алгоритм завершує роботу через скінченну кількість кроків, якщо множина диз’юнктів S незагальнозначима, або працює нескінченно довго в протилежному випадку, при умові нескінченності ербранівського базису для S.

Розглянемо послідовність операторів мови як синтаксичну формулу:

do

<послідовність операторів>

assign(<проблемна змінна>,<значення проблемної змінної>)

<послідовність операторів>

while(<логічна формула>)

Присвоєння значення проблемній змінній може призвести до “зациклювання” композиційної схеми навіть при умові незагальнозначимості логічної формули.

Список використаних джерел:

1. Провотар А.И., Барткив А.Б. Верификация композиционных схем в CASE APS // Программно-алгоритмическое обеспечение решения задач прикладной математики. — Киев: Ин-т кибернетики им. В.М. Глушкова АН Украины. — 1993. — С. 43-47.

2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем: Пер. с англ. — М.: Наука, 2013. — 360 с.



Creative Commons Attribution Ця робота ліцензується відповідно до Creative Commons Attribution 4.0 International License

допомогаЗнайшли помилку? Виділіть помилковий текст мишкою і натисніть Ctrl + Enter


 Інші наукові праці даної секції
СТАТИСТИЧНИЙ АНАЛІЗ РИНКУ КРИПТОВАЛЮТ
26.09.2021 15:31
СТРАТЕГІЧНІ ТРЕНДИ РОЗВИТКУ ІТ-ІНДУСТРІЇ ТА ТЕХНОЛОГІЙ
26.09.2021 15:20
ОСОБЛИВОСТІ ОРГАНІЗАЦІЇ РОБОЧОГО МІСЦЯ СПЕЦІАЛІСТА В ГАЛУЗІ ІНФОРМАЦІЙНИХ ТЕХНОЛОГІЙ
15.08.2021 17:09




© 2010-2024 Всі права застережені При використанні матеріалів сайту посилання на www.economy-confer.com.ua обов’язкове!
Час: 0.203 сек. / Mysql: 1367 (0.156 сек.)