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

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

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

26 травня 2022

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



  Головна
Нові вимоги до публікацій результатів кандидатських та докторських дисертацій
Редакційна колегія. ГО «Наукова спільнота»
Календар конференцій
Наші збірники
  Наукові конференції
 
 Лінки
 Форум
Наукові конференції
Наукова спільнота - інтернет конференції
Світ наукових досліджень 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-2022 Всі права застережені При використанні матеріалів сайту посилання на www.economy-confer.com.ua обов’язкове!
Час: 0.132 сек. / Mysql: 812 (0.105 сек.)