Логіка у програмуванні

Умовно висловлюючись, можна сказати, що комп'ютер складається з матеріальної частини та математичного (програмного) забезпечення, або, використовуючи професійну лексику, з «заліза» і «взуття». І до того, і до іншого має саме безпосереднє відношення математична логіка, ні перше, ні друге без математичної логіки обійтися не можуть.

Математична логіка та розвиток інформатики

У свою чергу, інформатика як наука почала формуватися разом з створенням і бурхливим розвитком обчислювальної техніки. Її формування і визначення її предмета тривають по теперішній час. Інформатика — наука про зберігання, обробки і передачі інформації за допомогою комп'ютерів. Вона включає в себе великі розділи, які вивчають алгоритмічні, програмні та технічні засоби зберігання, обробки і передачі інформації. Математична логіка виявилася єдиною математичною наукою, методи якої стали найпотужнішими інструментами пізнання у всіх розділах інформатики. Тому скільки- серйозне вивчення інформатики немислимо без освоєння основ математичної логіки.

Щоб комп'ютер працював, він повинен бути оснащений програмним забезпеченням, тобто комплексом програм, що орієнтують комп'ютер на вирішення завдань того чи іншого класу. Слово «програма» має грецьке походження і означає "оголошення ", « розпорядження» . Уже саме поняття комп'ютерної програми, що передбачає чіткий алгоритмічний припис комп'ютера про порядок і характер дій, передбачає проникнення в програму, а також у процес її складання (в програмування) теорії алгоритмів . Але при більш пильному розгляді процес проникнення логіки в програми і програмування виявляється значно більш глибоким і органічним. Не тільки один розділ теорії алгоритмів працює тут, але виключно дієвим виявляється саме істота математичної логіки — її мову, її аксіоматичні теорії, висновки і теореми в них, властивості цих теорій.

Фундаментальна основа програмування

Теорія алгоритмів та математична логіка — фундаментальна основа програмування. У 30 -і рр. XIX ст. англійський математик Чарлз Беббедж висловив вперше ідею обчислювальної машини. І тільки сто років по тому логіки розробили чотири математично еквівалентні моделі поняття алгоритму. Саме в теорії алгоритмів були передбачені основні концепції, які лягли в основу принципів побудови і функціонування обчислювальної машини з програмним керуванням і принципів створення мов програмування. Ідею такої обчислювальної машини вперше змогли реалізувати болгарський учений С. Атанасов в 1940 р. і німецький вчений К. Цузе в 1942 р. Чотири головні моделі алгоритму породили різні напрямки в програмуванні.

Моделі поняття алгоритму

Перша модель — це абстрактна обчислювальна машина (А. Тьюринг, Р. Пост). Вона з'явилася абстрактним прообразом реальних обчислювальних машин. До цих пір всі обчислювальні машини в деякому сенсі базуються на ідеї Тьюринга: їх пам'ять фізично складається з бітів, кожен з яких містить або 0, або 1 . Програмне управління успадкувало від цих абстрактних машин і програму, вміщену в «постійну пам'ять» (ідея помістити програму ЕОМ в основну пам'ять, щоб мати можливість змінювати її в ході обчислень, належить Джону фон Нейманом), а структура команди сучасної ЕОМ в значній мірі нагадує структуру команди машини Тьюринга. У рамках теорії машин Тьюринга откристаллизовался найважливіші для комп'ютерних додатків логіки поняття: обчислювана функція, здійсненне завдання, нерозв'язна (алгоритмічно) задача. Зібрано велику кількість визначень абстрактних обчислювальних машин і показано, як кожне з них можна звести до іншого підходящої кодуванням входів і виходів.
Друга модель — це рекурсивні функції, ідея яких сходить до гильбертовськой аксиоматическому підходу. Від них успадкувало свої основні конструкції сучасне структурне програмування.
Третій спосіб опису алгоритмів — нормальні алгоритми А. А. Маркова. Вони послужили основою мови Рефал і багатьох інших мов обробки символьної інформації.
Четвертий напрямок в теорії алгоритмів — так зване λ -числення — базується на ідеях радянського логіка Р.Шейнфінкеля та американського логіка X. Б. Каррі. Виявилося, що для визначення всіх вичіслімих функцій досить операцій так званої λ — абстракції і суперпозиції. Ідеї λ -числення активно розвиваються в мові Лісп, функціональному програмуванні і в багатьох інших перспективних напрямах сучасного програмування.

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

Опис комп'ютерних програм за допомогою математичної логіки

Перші спроби застосувати в програмуванні розвинені логічні обчислення і методи формалізації зробив американський логік X. Б. Каррі. У 1952 р. він зробив доповідь «Логіка програмних композицій», ідеї якої випередили свій час принаймні на чверть століття. Каррі розглянув задачу програмування, як завдання складання більших програм з готових шматків. Було введено дві базисні системи конструкцій: перша — послідовне виконання, розгалуження і цикл, друга — послідовне виконання і умовний перехід. Він охарактеризував логічні засоби, які можна використовувати для композиції програм з підпрограм в кожному з цих випадків.

Як відомо, комп'ютер є свого роду «ідеальним бюрократом»: він не сприйме програму, написану на не до кінця формалізованою мовою, і приступить до роботи лише після того, як все виражено в повній відповідності з детальними інструкціями. Тому в 1960 -і рр. на перший план вийшли завдання точного визначення формальних мов досить складної структури. Математична логіка, підтримувана ідеями програмування, успішно з ними впоралася, розробивши опис синтаксису складних і багатих виражальними засобами формальних мов.

У середині 1960 -х рр. практично одночасно з'явився ряд піонерських робіт у галузі опису умов, яким задовольняє програма. Радянський математик В. М. Глушков в 1965 р. ввів поняття алгоритмічної алгебри, що послужило прообразом алгоритмічних логік. Ф. Енгелер в 1967 р. запропонував використовувати мови з нескінченно довгими формулами, щоб висловити нескінченну безліч можливостей, що виникають при різних виконаннях програми. Але найбільшу популярність придбали мови алгоритмічних логік. Ці мови були винайдені практично одночасно американськими логіками Р. У. Флойдом (1967), С. А. Р. Хоаром (1969) і вченими польської логічної школи, наприклад А. Сальвіцкім (1970) та ін.

Алгоритмічна логіка (або динамічна логіка, або програмна логіка, або логіка Хоара) — розділ теоретичного програмування, в рамках якого досліджуються аксіоматичні системи, що представляють засоби для завдання синтаксису і семантики мов програмування, а також для синтезу комп'ютерних програм та їх верифікації (перевірки правильності роботи). Мови алгоритмічних логік грунтуються на логіці предикатів 1 -го порядку і включають в себе висловлювання виду { A } S { B }, читающиеся наступним чином: «Якщо до виконання оператора S було виконано A, то після нього буде виконано B». Тут A називається передумовою, B — післяумовою, або обіцянкою S. На цій мові даються логічні описання операторів присвоєння та умовного переходу, розгалуження, циклу.

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

Динамічна логіка є одним з типів логічних систем, що використовуються для логічного синтезу комп'ютерних програм. Логічний синтез — один із способів переходу від специфікації програми до реалізуючого алгоритму, що має форму точного міркування в деякій логічній системі. У динамічній логіці специфікація завдання задається у вигляді двох формул обчислення предикатів — передумови і післяумови, а аксіомами логічної системи є схеми передумови та післяумови, що пов'язуються тими чи іншими конструкціями мови програмування. Синтезована програма виходить у формі виведеного в динамічної логікою твердження, яка говорить, якщо аргументи завдання задовольняють задану передумову, то результат виконання синтезованої програми задовольняє задану постумову.

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

Принципово інший спосіб визначення семантики програм, придатний, скоріше для опису всієї алгоритмічної мови, а не конкретних програм, запропонував в 1970 р. американський логік Д. Скотт. Він побудував математичну модель λ -числення і показав, як переводити функціональний опис мови структурного програмування в λ -числення і як визначити математичну модель алгоритмічного мови через модель λ-числення. Ця так звана денотаційна семантика алгоритмічних мов, стала практичним інструментом побудови надійних трансляторів із складних алгоритмічних мов. Так іще одна абстрактна область математичної логіки знайшла прямі практичні застосування.

Опис програмування та аналіз його концепцій за допомогою математичної логіки

Програмування — це процес складання програми, плану дій. Було відмічено, що класична логіка погано підходить для опису цього процесу хоча б тому, що вона погано підходить взагалі для опису всякого процесу в математиці. Ще на початку XX ст. стало ясно, що в математиці давно розійшлися поняття «існувати» і «бути побудованим», з античних часів трактовавшиеся як синоніми. Були виявлені так звані математичні об'єкти — «привиди» (множини, Функції, числа), існування яких доведено, але побудувати які можна. Причиною їх появи з'явився ефект поєднання класичної логіки з теоремою Геделя про неповноту формальної арифметики. Один з фундаментальних законів класичної логіки — закон виключеного третього (P ˅ ˥P) в деякому вільному трактуванні фактично означає, що ми знаємо все. Цей постулат звичайно ж ніяк не можна назвати реалістичним: ми знаємо надзвичайно мало, і чим більше дізнаємося, тим краще це розуміємо. Голландський математик Л. Е. Я. Брауер визначив логічні коріння «привидів», ще до відкриття теореми Геделя, в 1908 р., і почав побудову так званої інтуїтивної математики, яка не приймає закон (P ˅ ˥P), як універсальний. У 1930–1932 рр. другий голландець А. Гейтинг строго сформулював логіку, якою користувалися в інтуїтивній математиці — інтуїтивну логіку. Її математична інтерпретація, викладена радянським математиком А. М. Колмогоровим зберегла своє значення до цих пір.

А. М. Колмогоров розглянув логіку як числення завдань. Кожна формула алгебри висловлювань розглядається не просто як формула, а як вимога вирішити завдання, тобто побудувати об'єкт, що задовольняє деяким умовам. Це так звана конструктивна інтерпретація логіки висловлювань. Логічні зв'язки розуміються як засоби побудови формулювань більш складних завдань з простіших, аксіоми — як завдання, вирішення яких дано, правила виводу — як способи перетворення рішень одних завдань у вирішення інших. Відзначимо, що рішення задачі — це не тільки сам шуканий об'єкт, а й доказ того, що він задовольняє пропонованим вимогам. Наприклад, формула A ˄ B розуміється в колмогорівській інтерпретації як завдання, яке полягає в тому, щоб побудувати розв'язок завдання A та розв'язок завдання B, правило висновку A , B \ A ˄ B — як перетворення, яке будує з об'єкта а, розв'язок завдання A , та об'єкта b, розв'язок завдання B, пару (a, b), розв'язок завдання A ˄ B. Об'єкт a, розв'язує завдання, зіставлене формулою A, називається реалізацією A. Цей факт позначається aRA. Центральним моментом конструктивного розуміння логічних формул є інтерпретація імплікації. Конструктивна імплікація A → B розуміється, як вимога побудувати ефективне перетворення f, застосоване до всіх реалізацій формули A і переводить їх у реалізації формули B.

Нечітке колмогорівське формулювання логіки, як обчислення завдань, породила численні різні конкретизації, давши цілу систему точних математичних визначень. Це формулювання знайшло застосування не тільки в інтуїтивній логіці, для якої вона була створена, а й в інших логічних системах. Строгі математичні семантики, засновані на ідеї Колмогорова, зазвичай називають семантиками реалізованості (на відміну від інших видів логічних семантик, які базуються на системах істиннісних значень). Першу реалізованість побудував американський логік С. К. Кліні в 1940 р. для арифметики з інтуїтивною логікою. У 1960-1980- х рр. з'явилися десятки понять реалізованості, як для систем, що базуються на інтуїтивній логіці, так і для інших логік. Радянський логік А. А. Воронков в 1985 р. вивів умови, при яких класична логіка може розглядатися як конструктивна. З них, зокрема, випливає, що необхідною (але не достатньою) умовою конструктивності класичної теорії є її повнота, тобто виводимість в ній для кожної замкнутої формули F або самої F, або її заперечення ˥F. Тим самим ще раз підтвердилося прозріння Брауера щодо логічних коренів неконструктивності. Зауважимо, що прикладами класичних теорій, що мають конструктивне тлумачення, служать елементарна геометрія і алгебраїчна теорія дійсних чисел.

Опис програмування за допомогою логіки засноване на певній аналогії між висновком формули в деякому логічному обчисленні і програмою вирішення завдання, що відповідає цій формулі при конструктивній інтерпретації логіки. Логічна теорія, відповідна структурним схемам програм, з'явилася в середині 1980 -х рр. Структурні схеми відповідали нарождающемуся новому типу логіки — логіки схем програм, якою користується програміст для створення складних, багатоваріантних, ітеративних планів дій.

Верифікація програм за допомогою математичної логіки

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

Тому винятково важливе завдання суворого доведення правильності програм, і саме для цієї мети і почали розроблятися програмні та динамічні логіки.

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

Сформулюємо тепер точне визначення поняття правильності програми. Нехай α — програма, P — твердження, що відноситься до вхідних даних, яке має бути істинно перед виконанням програми α (воно називається передумовою програми α), Q — твердження, яке має бути істинно після виконання програми α(воно називається післяумовою програми α). Розрізняють два види правильності програм: часткову і тотальну (повну). Програма α називається частково правильною щодо передумови P і післяумови Q, якщо кожен раз, коли перед виконанням α передумова P істинна для вхідних значень змінних, і α завершує роботу, післяумова Q також буде істинною для вихідних значень змінних. У цьому випадку будемо використовувати запис P [ α ] Q. Програма α називається тотально правильною відносно P і Q, якщо вона частково правильна відносно P і Q, і α обов'язково завершує свою роботу для вхідних значень змінних, які відповідають умові P. У цьому випадку пишемо P [ α! ] Q.

Звернемо увагу на те, що поняття правильності програми α сформульовано щодо відповідних тверджень (умов) P і Q. Тому з істинності твердження P [ α ] Q (або P [ α ! ] Q відповідно) не обов'язково слідує істинність твердження про правильність програми при інших передумовах та післяумовах. Аналогічним чином, заміна в P [ α ] Q (або P [ α ! ] Q) програми α на програму β, взагалі кажучи, не зберігає істінностного значення твердження про правильність. Не слід також думати, що за даних умов P і Q існує тільки одна програма α, для якої висловлення P [ α ] Q (або P [ α ! ] Q) істинно.

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

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

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

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

Одна з модифікацій методу Флойда полягає в побудові кінцевої аксіоматичної системи (так званої «логіки Хоара»), що складається з схем аксіом і правил виводу, в якій в якості теорем виводяться твердження про часткову правильності програм, зокрема на мові програмування Паскаль. Така система використовується і для завдання аксіоматичної семантики мови Паскаль. Аксіоматичні системи, родинні логіці Хоара, розроблені і для інших алгоритмічних мов програмування.

Для доказу правильності рекурсивних програм використовується метод математичної індукції, пов'язаний з визначенням найменшої нерухомої точки, а для програм зі складними структурами даних (наприклад, графами, деревами) — індукція за структурою даних. При цьому в теоретичних дослідженнях за логікою Хоара розглядаються звичайні властивості Аксіоматизації в логіці — їх несуперечність і повнота.

Джерела

Список використаної літератури

Математическая логика и теория алгоритмов, Игошин В. И., 2008
Колмогоров А. Н., Драгалин А. Г. Математическая логика. Изд. 3-е, 2006.
П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация).

Див. також