Главная Контакты Добавить в избранное Авторы Вопросы и ответы
,

УДК 004.421.6

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

Львов М.С.

Вступ

Комп'ютерні програми, у яких реалізовані розв’язання фізичних задач, мають задовольняти декільком специфічним властивостям. Наведемо деякі із них:

1. Розмірності фізичних величин. Оскільки обчислення в таких програмах засновані на формулах фізичних законів, відповідні змінні, крім ідентифікатора, типу та значення, мають ще одну характеристику – фізичну розмірність. Сучасні мови програмування не використовують за замовчуванням ні типізації змінних за їх фізичним змістом, ні, тим більше, фізичних розмірностей констант і змінних. Тому помилки в програмах, пов'язані з неправильним використанням фізичних розмірностей, не виявляються ні під час компіляції, ні під час виконання програми. Таким чином виникає задача перевірки правильності використання змінних за їх фізичними розмірностями. Цю задачу потрібно вирішувати методами статичного аналізу програмного коду. Користувач має специфікувати всі змінні програми фізичними розмірностями, а аналізатор має перевірити правильність цієї специфікації. Звичайно, аналіз програмного коду має спиратися на співвідношення, які визначені фізичними законами й правилами систем фізичних розмірностей. Наприклад, співвідношення Вольт = Ампер * Секунда - закон Ома в системі СІ.

2. Межі змінення фізичних величин. Результати обчислень, здійснюваних програмою, використовуються в реальних фізичних приладах і пристроях. Тому значення змінних не можуть бути довільними - вони мають перебувати в межах, установлених параметрами приладу або пристрою. Наприклад, у кожному електричному приладі є гранично припустима споживана потужність. Якщо її перевершити, прилад згорить. Помилки в програмах, пов'язані з виходом значень змінних за межі припустимих значень, також не можуть бути виявлені ні під час компіляції, ні під час виконання програми. Цю задачу також потрібно вирішувати методами статичного аналізу програмного коду. Користувач має специфікувати всі змінні програми границями їхніх припустимих значень, а аналізатор має перевірити правильність цієї специфікації.

3. Виконання законів збереження. У фізиці існують фундаментальні закони – так звані закони збереження. Це, наприклад, закон збереження енергії. Можна припустити, що ці закони виражаються співвідношеннями типу рівності між деякими змінними програми. У теорії програмування такі співвідношення називають програмними інваріантами. У правильно написаних програмах інваріанти мають виконуватися у визначених контрольних точках програми незалежно від шляху обчислень і початкових значень змінних. Помилки, допущені у формулах програми, приводять до невиконання цієї умови. Як і у попередніх задачах, помилки такого роду не можуть бути виявлені ні при компіляції, ні під час виконання програми. Задача доведення інваріантності рівності, заданої користувачем у даній контрольній точці програми, вирішується методами статичного аналізу [1-3].

У даній роботі описано алгоритм розв’язання другої з цих практичних задач статичного аналізу програм - задачі перевірки правильності границь змінення змінних у послідовних програмах. Алгоритм використовує базиси Гребнера [4] й методи відділення дійсних коренів поліномів [5].

Постановка задачі

Нехай  - вектор змінних програми  Оператор присвоєння  будемо записувати у виді , де  - деякий алгебраїчний вираз.

                                                             (1)

Послідовною програмою будемо називати послідовність операторів присвоєння

Кожній змінній  припишемо область її визначення – числовий інтервал , , де  - множина раціональних чисел. Через  позначимо декартовий добуток . Для оператора присвоєння (1) через  позначимо числову множину, визначену формулою

.                                                 (2)

            Таким чином, - множина значень змінної – лівої частини оператора (1), якщо вектор - аргумент його правої частини пробігає усю множину визначення вектора змінних  програми.

Насправді ми будемо розглядати оператор присвоєння як оператор, що відображає , причому зміненню піддається тільки -та координата. Отже, можна вважати,  що   Далі, визначимо множину  формулою

                                                (3)

Тепер задачу перевірки правильності границь змінення змінних в програмі можна визначити співвідношенням

                                                                                (4)

Зауваження 1. Насправді  ця задача очевидним чином зводиться до серії задач

                                                                          (5)

Це означає, що її достатньо розв’язати для одного оператора присвоєння (1):

                                                                               (6)

Зауваження 2. У загальній постановці задачу треба було б розглядати для довільних програм, контролюючі діапазони змінення змінних у довільних контрольних точках. Однак, з нашої точки зору, задача у такій постановці є дуже складною і може виявитися навіть алгоритмічно нерозв’язною. Тим не менш, якщо точними методами статичного аналізу буде доведено, що будь-який оператор присвоєння  довільної програми задовольняє умові (5), у довільній контрольній точці програми вектор значень змінних програми буде знаходитися у заданому діапазоні. 

Отже, задачу, яка розв’язується у роботі, можна сформулювати таким чином:

Нехай - функція дійсних змінних . Визначити, чи належить заданому відрізку ?                                                                                                     

Алгоритми, розглянуті нижче, істотно залежать від виду функції . Якщо - поліном, задачу будемо називати визначеною поліноміально. Якщо - раціональна функція, задачу будемо називати визначеною раціонально. Якщо ж формула  містить радикали, задача є радикально визначеною. Ми розглянемо спочатку поліноміально визначені задачі, потім – раціонально визначені задачі, і, нарешті – радикально визначені задачі. Ми будемо також вважати, що коефіцієнти  - суть раціональні числа.

Математичне обґрунтування алгоритму

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

1. Метод побудови системи алгебраїчних рівнянь для координат критичних точок відображення. Позначимо через  точку . Нехай у точці  функція   досягає найбільшого (найменшого) значення. Тоді

1.      або

 ,                                                          (7)

2. або точка належить границі паралелепіпеда

Таким чином, алгоритм пошуку критичних та екстремальних точок функції  на множині  може бути заснований на переборі всіх можливих варіантів. Кожний з варіантів визначений підмножиною координат, для яких координатні змінні приймають граничні значення  або . Назвемо такі координати граничними. Для інших координат (назвемо їх внутрішніми) у цьому варіанті потрібно розглядати систему співвідношень (7).  Відзначимо, що загальна кількість варіантів дорівнює .

Будемо вважати, що в даному варіанті необхідні граничні значення змінних уже підставлені в поліном  і результат приведений до канонічного виду. Цей результат ми також будемо позначати через . Покладемо , . (На практиці корисно звільнити поліноми  від квадратів.) Отже,  (7) – система цілих алгебраїчних рівнянь .

2. Метод побудови мінімального полінома для k-ої координати множини критичних точок. Побудуємо базис Гребнера ідеалу , елімінуючи послідовно змінні . Для простоти позначень покладемо . Як відомо [4], базис Гребнера має «трикутний» вид. Запишемо відповідну систему рівнянь:

                                                   (8)

Система рівнянь (8) рівносильна системі (7), а дійсні корені  рівняння   - суть відповідні координати критичних екстремальних точок .

3. Метод відділення координат критичних точок на відрізку. Ці корені можуть бути відділені на відрізку   з наперед заданою точністю за допомогою, наприклад, алгоритму Штурма [5] (див. Рис.1) 

 
 
 

 

 

 


Рис 1. Відділення коренів

На цьому рисунку позначені корені  й кінці числових відрізків , що відокремлюють ці корені на розглянутому відрізку. (Для простоти в позначеннях опущений індекс .). Для кожного  можна отримати такі відрізки, що

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

4. Метод побудови образів множин критичних точок і кандидатів у критичні точки відображення. Розглянемо множину  точок виду простору , кожна координата яких – дійсний корінь відповідного полінома  на відрізках . Ці точки – суть кандидати в критичні точки полінома  проекції паралелепіпеда  на підпростір, визначений внутрішніми координатами. Пояснимо ситуацію ілюстрацією на графіку для частинного випадку :

Рис 2. Множина точок - кандидатів у критичні точки

 

Припустимо, що отримана трикутна система рівнянь має вигляд  причому  і усі її корені дійсні. Тоді множину розв’язків системи, оскільки вона є трикутною, можна записати у вигляді  (на рис.2 – чорні точки). У результаті перетворення системи до діагонального виду виключенням  одержимо систему , причому . Тому кандидатами в критичні точки будуть усі пари  На рисунку ми бачимо, що серед кандидатів у критичні точки 4 точки є помилковими. На графіку вони відзначені квадратиками.

Проте, оскільки всі кандидати в критичні точки належать паралелепіпеду , задача  еквівалентна задачам

Розглянемо систему рівнянь

                                                   (9)

Елімінуючи послідовно в цій системі змінні  методом побудови базису Гребнера, отримуємо у якості останнього поліном базису  Легко бачити, що серед коренів цього полінома – усі образи множини критичних точок  .

Розглянемо знову систему рівнянь (9). Оскільки ця система зведена до трикутного виду, до неї можна застосувати процедуру діагоналізації, виключаючи недіагональні змінні тим же методом базисів Гребнера. У результаті одержимо систему  

                                                        (10)

Елімінуючи послідовно в системі (10) змінні  методом побудови базису Гребнера (як у попередньому випадку), одержуємо як останній поліном базису поліном  Легко бачити, що серед коренів цього поліному – усі кандидати в критичні точки.

5. Метод побудови відповідності «множина критичних точок – образ цієї множини». Проблема полягає в тім, щоб співвіднести кожному елементу множини корінь  числа виду . Розглянемо рис. 3, що ілюструє сказане вище.

Рис. 3. Множина критичних точок та її образ

 

Апріорі можливі кілька варіантів реалізації співвідношення  Один із цих варіантів показаний на рис.3. чорними кружками, другий – не заштрихованими квадратиками.

1-ий варіант: .

2-ой варіант: .  

У першому варіанті з . У другому варіанті ця властивість не виконується.  

Нехай  і . Тоді

                                         (11)

де  - деякий набір точок з паралелепіпеда з головною діагоналлю . Звідси випливає нерівність

                                                   (12)

Значення частинних похідних можна ефективно оцінити через значення границь паралелепіпеда , на якому ми розглядаємо задачу:

Тому

                                                  (13)

Нерівність (7) ми будемо використовувати для визначення відповідності

                                                      (14)

за наступним алгоритмом. 

6. Основний алгоритм

Нехай  - множина розв’язків системи (4)  і  відповідно точки множини , визначені  у п.3.       

6.1. Відокремимо точки множини паралелепіпедами такими, що , а довжини ребер не перевершують даного додатного числа .

6.2. Відокремимо також точки  множини  відрізками , довжини яких не перевершують даного додатного числа .

6.3. Виберемо в паралелепіпеді точку  з раціональними координатами й обчислимо  Використаємо нерівність (12) для точок у правій частині (12).

                                               (15)

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

 

Рис 4. Правило 3-х епсілон

 

Таким чином, точка має належати відрізку  .

Правило 3-х епсілон

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

Тоді визначення відповідності (13) виконується за допомогою основного алгоритму, у якому  обрані за правилом 3-х епсілон.

6.4. Якщо корінь полінома  й точки множини кандидатів у критичні точки відділені з дотриманням правила 3-х епсілон, всі точки  мають належати відрізку . Тоді  належить заданому відрізку. Інакше виконується заперечення цього співвідношення.

Раціонально визначені задачі

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

      Якщо відокремлюючий  паралелепіпед деякого дійсного кореня знаменника  входить до , функція  необмежена на . В іншому разі (другий етап) задача розв’язується цілком аналогічно до поліноміально визначеної задачі, причому у якості поліномів  треба брати поліноми

                                                           (16)

Алгебраїчно визначені задачі

      Для радикально визначених задач формула функції  містить радикали:

. Цей вираз можна перетворити наступним чином:

.

В наших задачах для парних значень  додатково треба врахувати невід’ємність підкореного виразу. Таким чином, для задач над дійсними числами маємо 

Отже, функцію  на області  або на області визначено таким чином:

                                                   (17)

Можна дещо узагальнити (17) вважаючи, що другий кон’юнкт має загальний вид поліноміальної рівності від змінних .

                                                     (18)

Тоді частинні похідні функції  на  обчислюються з формул

()()             (19)

Отже,

()                       (20)

З системи рівнянь (20) можна виключити змінну , побудувавши скорочений базис Гребнера. В результаті отримаємо рівняння , яке грає роль рівняння (7) в алгоритмі розв’язання нашої задачі.   

Висновки

Основний алгоритм, принципи побудови якого описані вище, є досить неефективним. От основні причини неефективності:

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

2. У кожному варіанті будується множина точок – кандидатів у критичні точки. Насправді потрібно знайти тільки дві точки – точку найбільшого максимуму й точку найменшого мінімуму. Для цього досить перебрати множину всіх критичних точок, тобто множину розв’язків системи (9). Однак безпосередньо відокремити точки цієї множини важко. Для цього потрібно було б навчитися відокремлювати корінь по координаті  рівняння виду  за умови, що вже відокремлено корені . Однак аналог методу Штурма для такої постановки задачі нам невідомий. Тому доводиться будувати набагато більшу множину точок, що перебираються - кандидатів у критичні точки.

3. Ще один шлях – поліпшення оцінки (15) залежності  від : у нерівності  константу  потрібно вибрати якомога малою. Тоді зменшиться кількість кроків в алгоритмі відокремлення коренів.

ЛІТЕРАТУРА

1.                  M.S. Lvov. Invariant equalities of small degrees in programs, defined above field // Cybernetics. - 1988. - №1. - P. 108 - 110.

2.                  A.Letichevsky, M.Lvov. Discovery of invariant Equalities in Programs over Data fields. Applicable Algebra in Engineering, Communication and Computing. – 1993. – №4. – pp. 21-29.

3.                  M.Lvov. About one algorithm of program polynomial invariants generation. M. Giese, T. Jebelean. (Eds). Proc. Workshop on Invariant Generation, WING 2007. Technical report no. 07-07 in RISC Report Series, University of Linz, Austria. 06 2007. Workshop Proceedings. pp.85-99 (electronic).

4.                  Б.Бухбергер. Базисы Гребнера. Алгоритмический метод в теории полиномиальных идеалов. В кн.. Компьютерная алгебра. Символьные и алгебраические вычисления: пер. С англ../Под ред. Б.Бухбергера, Дж.Коллинза, Р.Лооса.-М.:Мир, 1986.-392 с., ил. сс. 331-383.

5.                  Дж.Коллинз, Р.Лоос. Вещественные нули полиномов. В кн.. Компьютерная алгебра. Символьные и алгебраические вычисления: пер. С англ../Под ред. Б.Бухбергера, Дж.Коллинза, Р.Лооса.-М.:Мир, 1986.-392 с., ил.  сс. 112-126.

 





Ответы на вопросы [_Задать вопроос_]

Информационно-управляющие комплексы и системы

Теленик С.Ф., Ролік О.І., Букасов М.М., Андросов С.А. Генетичні алгоритми вирішення задач управління ресурсами і навантаженням центрів оброблення даних

Богушевский В.С., Сухенко В.Ю., Сергеева Е.А., Жук С.В. Реализация модели управления конвертерной плавкой в системе принятия решений

Бень А.П., Терещенкова О.В. Применение комбинированных сетевых методов планирования в судоремонтной отрасли

Цмоць І. Г., Демида Б.А., Подольський М.Р. Методи проектування спеціалізованих комп’ютерних систем управління та обробки сигналів у реально-му час

Теленик С.Ф., РолікО.І., Букасов М.М., РимарР.В., Ролік К.О. Управління навантаженням і ресурсами центрів оброблення даних при виділених серверах

Селякова С. М. Структура інтелектуальної системи управління збиральною кампанією

Еременко А.П., Передерий В.И. Принятие решений в автоматизированных системах с учетом психофункциональных характеристик оператора на основе генетических алгоритмов

Ляшенко Е.Н. Анализ пожарной опасности сосновых насаждений в зоне Нижне-днепровских песков – самой большой пустыни в Европе

Кучеров Д.П., Копылова З.Н. Принципы построения интеллектуального автору-левого

Касаткина Н.В., Танянский С.С., Филатов В.А. Методы хранения и обработки нечетких данных в среде реляционных систем

Ходаков В.Е., Жарикова М.В., Ляшенко Е.Н. Применение когнитивного подхода для решения задачи поддержки принятия управленческих решений при ликвидации лесных пожаров

Гончаренко А.В. Моделювання впливу ентропії суб’єктивних переваг на прийняття рішень стосовно ремонту суднової енергетичної установки

Фарионова Н.А. Системный подход построения алгоритмов и моделей систем поддержки принятия решений при возникновении нештатных ситуаций

Биленко М.С., Серов А.В., Рожков С.А., Буглов О.А. Многоканальная система контроля качества текстильных материалов

Мотылев K.И., Михайлов M.В., Паслен В.В. Обработка избыточной траекторной информации в измерительно-вычислительных системах

Гончаренко А.В. Вплив суб’єктивних переваг на показники роботи суднової енергетичної установки

Гульовата Х.Г., Цмоць І.Г., Пелешко Д.Д. Архітектура автоматизованої системи моніторингу і дослідження характеристик мінеральних вод

Соломаха А.В. Разработка метода упреждающей компенсации искажений статорного напряжения ад, вносимых выходными силовыми фильтрами

ПотапенкоЕ.М., Казурова А.Е. Высокоточное управление упругой электромеханической системой с нелинейным трением.

Кузьменко А.С., Коломіц Г.В., Сушенцев О.О. Результати розробки методу еквівалентування функціональних особливостей fuzzy-контролерів

Кравчук А. Ф., Ладанюк А.П., Прокопенко Ю.В. Алгоритм ситуационного управления процессом кристаллизации сахара в вакуум-аппарате периодического действия с механическим циркулятором

Абрамов Г.С., Иванов П.И., Купавский И.С., Павленко И.Г. Разработка навигационного комплекса для автоматического наведения на цель системы груз-управляемый парашют

Литвиненко В.И., Четырин С.П. Компенсация ошибок оператора в контуре управления следящей системы на основе синтезируемых вейвелет-сетей

Бардачев Ю.Н., Дидык А.А. Использование положений теории опасности в искусственных иммунных системах

Рожков С.О., Кузьміна Т.О., Валько П.М. Інформаційна база як основа для створення асортименту лляних виробів.

Ускач А.Ф., Становский А.Л., Носов П.С. Разработка модели автоматизированной системы управления учебным процессом

Мазурок Т.Л., Тодорцев Ю.К. Актуальные направления интеллектуализации системы управления процессом обучения.

Ускач А.Ф., Гогунский В.Д., Яковенко А.Е. Модели задачи распределения в теории расписания.

Сідлецький В.М., Ельперін І.В., Ладанюк А.П. Розробка алгоритмів підсистеми підтримки прийняття рішень для контролю якості роботи дифузійного відділення.

Пономаренко Л.А., Меликов А.З., Нагиев Ф.Н. Анализ системы обслуживания с различными уровнями пространственных и временных приоритетов.

Коршевнюк Л.О. Застосування комітетами експертів системи нечіткого логічного виводу із зваженою істинністю.. – С. 73 – 79.

Кирюшатова Т.Г., Григорова А.А Влияние направленности отдельных операторов и направленности всей группы на конечный результат выполнения поставленной задачи.

Петрушенко А.М., Хохлов В.А., Петрушенко І.А. Про підключення до мови САА/Д деяких засобів паралельного програмування пакету МРІСН.

Ходаков В.Е., Граб М.В., Ляшенко Е.Н. Структура и принципы функционирования системы поддержки принятия решений при ликвидации лесных пожаров на базе новых геоинформационных технологий.

Сидорук М.В., Сидорук В.В. Информационные системы управления корпорацией в решении задач разработки бюджета.

Нагорный Ю.И. Решение задачи автоматизированного расчета надежности иасуп с использованием модифицированного метода вероятностной логики

Козак Ю.А. Колчин Р.В. Модель информационного обмена в автоматизированной системе управления запасами материальных ресурсов в двухуровневой логистической системе

Гожий А.П., Коваленко И.И. Системные технологии генерации и анализа сценариев

Вайсман В.А., Гогунский В.Д., Руденко С.В. Формирование структур организационного управления проектами

Бараненко Р.В., Шаганян С.М., Дячук М.В. Аналіз алгоритмів взаємних виключень критичних інтервалів процесів у розподілених системах

Бабенко Н.И., Бабичев С.А. Яблуновская Ю.А. Автоматизированная информационная система управления учебным заведением

Яковенко А.Е. Проектирование автоматизированных систем принятия решений в условиях адаптивного обучения с учетом требований болонского процесса

Бараненко Р.В Лінеаризація шкали і збільшення діапазону вимірювання ємностей резонансних вимірювачів

Головащенко Н.В. Математичні характеристики шумоподібно кодованих сиг-налів.

Шерстюк В.Г. Формальная модель гибридной сценарно-прецедентной СППР.

Шекета В.І. Застосування процедури Append при аналізі абстрактних типів даних модифікаційних запитів.

Цмоць І.Г. Алгоритми та матричні НВІС-структури пристроїв ділення для комп'-ютерних систем реального часу.

Кухаренко С.В., Балтовский А.А. Решение задачи календарного планирования с использованием эвристических алгоритмов.

Бараненко Р.В., Козел В.Н., Дроздова Е.А., Плотников А.О. Оптимизация рабо-ты корпоративных компьютерных сетей.

Нестеренко С.А., Бадр Яароб, Шапорин Р.О. Метод расчета сетевых транзакций абонентов локальных компьютерных сетей.

Григорова А.А., Чёрный С. Г. Формирование современной информационно-аналитической системы для поддержки принятия решений.

Шаганян С.Н., Бараненко Р.В. Реализация взаимных исключений критических интервалов как одного из видов синхронизации доступа процессов к ресурсам в ЭВМ

Орлов В.В. Оценка мощности случайного сигнала на основе корреляционной пространственной обработки

Коджа Т.И., Гогунский В.Д. Эффективность применения методов нечеткой логики в тестировании.

Головащенко Н.В., Боярчук В.П. Аппаратурный состав для улучшения свойств трактов приёма – передачи информации в системах промышленной автоматики.