Теорія програмування

Вступ

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

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

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

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

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

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

Нехай   - Вектор змейных програм  P  Оператор присвоения  S  будет записывать в вид  , де  ф  - деякий алгебраический вид.

                                                                                              (1)

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

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

. (2)

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

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

                    (3)

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

                                       (4)

Замечено 1.  Направление задачи очевидным образом приводит к решению серії задач

                                  (5)

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

                                         (6)

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

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

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

Алгоритмы, проверяют нижние, стотно залежать от видимых функций  F(x) . Якщо  F(x) - полином, размеры будут називати визначеною полиномиально. Якщо  F(x) - рациональная функция, размеры будут називати выделеною рационально. Якщо ж формула  F  містить радикали, задача є клетчатки выделеною. Мы проверяем, как распределяются полные значения задач, а затем – рационально определяются задачи, и, наоборот, определяются – определенные значения задач. Мы будем також вважати, що коефіцієнти   - суть рациональных чисел.

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

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

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

1.  або  , (7)

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

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

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

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

                         (8)

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

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

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

Индексы, которые могут быть изменены автоматически, аналогичны значениям, которые могут быть заменены на внутренние координаты.

4.  Метод постройки образов множества критических токов и кандидатов в критических точках відображення . Просмотр множину В токе  видимости  , кожной координаты яких – дійсний корінь відповідного полінома   на відрізках   . Эти точки – основные кандидаты в точные точки зрения полінома f(X) проекта паралелепипеда  D  на підпростір, обозначенных кривыми внутрішніми координатами. Поясним ситуацию иллюстрации на графике для частичного випадку k = 2:

Рис 2. Множина точок - кандидат в критические точки зрения

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

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

Просмотр системного уровня

              (9)

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

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

               (10)

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

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

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

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

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

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

Нехай   я  . Тоді

                   (11)

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

             (12)

 Значення частичных похидних может быть эффективно проверена через обозначение границ паралелепипеда D, по какому-то

 ми смотровому боксу:

 Тому         (13)

Непрерывность (7) мы будем поддерживать для проверки достоверности  (14) за наступним алгоритмом.  

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

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

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

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

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

              (15)

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

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

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

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

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

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

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

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

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

         (16)

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

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

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

.

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

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

                       (17)

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

                     (18)

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

()&()             (19)

Отже,

&()                       (20)

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

Висновки

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

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

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

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

ЛІТЕРАТУРА

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.