Сторінка
4

Логіко-дедуктивне обґрунтування програмування

Цікаві надії плекає Р.Андерсон: "Якби можна було формалізувати довід правильності та проводити його абсолютно надійним взірцем (як автоматично доказовим пристроєм), то йому можна було б повністю довіряти. У майбутньому це, можливо, виявиться реальним, але не зараз" [7, 26].

Проаналізуємо ряд аспектів неможливості повного дедуктивного обґрунтування сучасних програм ЕОМ. Як відомо з теорем К. Геделя про неповноту логічних систем, неможлива повна формалізація жодної змістовної теорії. Якщо програма для ЕОМ буде побудована аксіоматично і буде розпочата спроба її формально-логічної побудови, то це завдання виявиться теоретично нездійсненним. А якщо врахувати, що жодна програма не може бути побудована за допомогою однієї аксіоматичної системи, то питання повної її формалізації відпадає. Крім цього, в процесі побудови формалізмів можуть бути пропущені логічні помилки, які важко з'ясовуються і які приведуть до побудови неправильних програм. Історичним прикладом такої помилки може служити теорема Х.Ербрана, доведена ним у 1930 р., на якій засновані найбільш розповсюджені машинні алгоритми. За допомогою цих алгоритмів здійснюється пошук доказів теорем математичної логіки. Ця важкоусувна помилка була виявлена тільки в 1963 р. Такого роду помилки в логічних побудовах програм ЕОМ можуть спостерігатися й в інших випадках. Їх можна усунути в результаті застосування іншого логіко-математичного апарату в процесі розвитку науки або практичної перевірки програм. "Але програма щодо доказу правильності програм, - відзначає А. І. Анісімов, - у свою чергу, має потребу в доводі правильності. Очевидно, в кінцевому підсумку правильність версифікуючої програми має бути доведена людиною" [8, 38]. Ієрархічна побудова програм для обґрунтування попередньої програми являє собою свого роду метапрограми різних рівнів. Для встановлення істинності попередньої програми, очевидне питання не теорії, а чисто практичне питання, людська практика повинна підтвердити істинність теоретичних висновків програмування.

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

При побудові програми важливим фактором є високий професіоналізм як у вивченні задачі, яку необхідно розв'язати, так і в самому логіко-математичному забезпеченні. З огляду на професійні труднощі, у наш час наукова думка спрямована на спеціалізацію і створення персональних ЕОМ - ПЕОМ. Персональні ЕОМ сприяють більш глибокому вивченню предметної галузі, тобто вивченню сутності речей. "Створений фахівцями у даній предметній галузі програмний продукт формалізує такі його тонкощі, які, по-перше, не вкладаються у традиційні моделі, по-друге, недоступні професіональним програмістам-виготовлювачам тиражованих пакетів прикладних програм" [9, 4].

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

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

Ще при виділенні визначеної задачі необхідно визначити поняття практичної видимості чи неозорості математичного твердження. Якщо математична задача зводиться до неозорої процедури, то важко гарантувати її істинність при побудові програм. У цьому випадку набирає сили діалектика кінцевого і нескінченного. "Неосяжна процедура, яка реалізується в істотній частині ЕОМ або допускає редукцію до досяжного доводу методами, які є у розпорядженні математиків" [10, 31]. Дійсно, кожен неозорий процес може бути помилковим, але ця помилка може бути виявлена при подальшій розробці і перевірці програм, розробці математичного забезпечення. В остаточному підсумку неможливо формалізувати цілком жоден процес. Справедливо зауважує Ю.І.Манін, що математичний світ має певну реальність і внутрішнє життя, що мало залежить від формалізмів, покликаних його описувати.

Ще слід зазначити могутні інтегративні властивості програмування й ЕОМ у науковому пізнанні. Програмування, машинна математика стали новим напрямком у науковому пізнанні. Вони сприяють проникненню в різні галузі людського знання, вони "стерли" грані між гуманітарними і природничо-науковими дисциплінами. Усі науки стали математизуватися за допомогою нової машинної математики, що дало новий імпульс у розвитку сучасного наукового знання.

Розглядаючи програмування як принципово новий метод у науковому пізнанні, академік В.М. Глушков відзначає, що цей математичний експеримент "займає проміжне місце між класичним дедуктивним методом і класичним експериментальним методом дослідження" [10, 32]. У зв'язку з цим можна говорити про новий напрямок у розвитку математики, який базується й на математичному формалізмі, й на здоровому глузді, що дозволяє зближати математику з експериментальними науками (природознавством, економікою та ін.). "У ХХ столітті математика перетворилась у своєрідну індустрію концептуальних систем будь-якої міри спільності, репрезентативної сили, інформаційної ємності, прогностичної могутності, пояснювального потенціалу" [11, 160]. Це сприяє збагаченню і розвитку як математики, так і математизованих наук. Вивчаючи дослідницькі можливості машинної математики, багато вчених схильні вважати, що вся історія розвитку математики є передісторією сучасної математики, що бурхливо розвивається, і має велике майбутнє як у розвитку самої математики, так і в математизації всього наукового знання.