UkrReferat.com
найбільша колекція україномовних рефератів

Всього в базі: 75838
останнє поновлення: 2016-12-03
за 7 днів додано 10

Реферати на українській
Реферати на російській
Українські підручники

$ Робота на замовлення
Реклама на сайті
Зворотній зв'язок

 

ПОШУК:   

реферати, курсові, дипломні:

Українські рефератиРусские рефератыКниги
НазваАлгоритмічна логіка Хоара (реферат)
АвторPetya
РозділЛогіка, формальна логіка, юридична логіка
ФорматWord Doc
Тип документуРеферат
Продивилось3359
Скачало620
Опис
ЗАКАЧКА
Замовити оригінальну роботу

Реферат на тему:

 

Алгоритмічна логіка Хоара

 

 

План

 

Вступ

 

Алгоритмічні логіки

 

Біографія Хоара

 

Алгоритмічна логіка Хоара

 

Аксіоми Хоара;

 

Приклад розв’язування задачі з використанням аксіом.

 

Висновок

 

Вступ

 

Логіка – це теорія, яка вивчає, як правильно потрібно міркувати,

правильно робити висновки, отримувати в результаті правильні

висловлювання. Тому логіка це наука, яка повинна містити список правил

отримання правильних висловлювань.

 

Алгоритмічні логіки

 

На початку 70-х років ХХ століття виникли алгоритмічні логіки. Вони були

створені з метою опису семантики мовою програмування.

 

Алгоритмічні логіки включають висловлювання вигляду

 

,

 

».

 

Ця логічна мова майже одночасно була створена Р.У.Флойдом (1967),

К.Хоаром (1969) і представниками польської логічної школи

(А.Сальвініцький та інші (1970)).

 

В 1969 році Хоар визначив просту мову програмування через логічну

систему аксіом і правила виведення для доведення часткової правильності

програми. В його роботі показано, що для визначення семантики мови не в

термінах виконання програми, а в термінах доведення її правильності

спрощує процес створення програми.

 

В 70-х роках на базі роботи Хоара починаються дослідження в області

аксіомних визначень мови програмування. З’являється багато робіт з

аксіоматизації різних конструкцій: від оператора присвоювання до різних

форм циклів, від виклику процедур до співпрограм. Головним недоліком

дослідників в ті роки було те, що вони не приділяли достатньо уваги

формальній логіці.

 

В 1972 році вийшла чергова стаття Хоара про доказ правильного подання

даних, що прискорило дослідження абстрактних типів даних. В СРСР роботи

в цій області проводились в Новосибірську (А.П.Єршов, В.Н.Агафонов,

А.В.Замулин, И.Н.Скопина).

 

В 1973 році були сформульовані правила доведення правильності для

більшості конструкцій мови Паскаль. В 1975 році була побудована

автоматична система «верификации для подмножества» мови Паскаль,

заснована на аксіомах і правилах виведення. В 1979 році була визначена

мова програмування Евкліда, в проект яого з самого початку була

закладена ідея аксіоматизації.

 

В 1976 році вийшла книга Е.Дейкстри «Дисципліна програмування», в якій

пропонується метод доведення правильності програми. Суть методу полягає

в тому, щоб будувати програму разом з доведенням, причому доведення

повинно випереджати побудову програми. Е.Дейкстр визначив для простої

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

використовувати в якості підрахування для виведення програми. Стало

зрозуміло, що користування формалізмом може призвести до побудови

програм більш надійним способом.» [3]

 

Біографія Хоара

 

Чарльз Ентоні Річард Хоар – британський вчений, який спеціалізується в

області інформатики і обчислювальної техніки. Найбільш відомий як

винахідник алгоритму «швидкого сортування» (1960), на сьогоднішній день

являється найпопулярнішим алгоритмом сортування.

 

Інші відомі результати його роботи: мова Z специфікацій і паралельна

модель взаємодії послідовних процесів (CSP, Communicating Sequential

-----> Page:

0 [1] [2]

ЗАМОВИТИ ОРИГІНАЛЬНУ РОБОТУ