Головна Головна -> Реферати українською -> Логіка -> Алгоритмічна логіка Хоара

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

Назва:
Алгоритмічна логіка Хоара
Тип:
Реферат
Мова:
Українська
Розмiр:
4,65 KB
Завантажень:
206
Оцінка:
 
поточна оцінка 5.0


Скачати цю роботу безкоштовно
Пролистати роботу: 1  2  3 
Реферат на тему:
Алгоритмічна логіка Хоара


План
Вступ
Алгоритмічні логіки
Біографія Хоара
Алгоритмічна логіка Хоара
Аксіоми Хоара;
Приклад розв’язування задачі з використанням аксіом.
Висновок


Вступ
Логіка – це теорія, яка вивчає, як правильно потрібно міркувати, правильно робити висновки, отримувати в результаті правильні висловлювання. Тому логіка це наука, яка повинна містити список правил отримання правильних висловлювань.
Алгоритмічні логіки
На початку 70-х років ХХ століття виникли алгоритмічні логіки. Вони були створені з метою опису семантики мовою програмування.
Алгоритмічні логіки включають висловлювання вигляду
,
які читаються: «Якщо до виконання оператором S було виконано , то після нього буде ».
Ця логічна мова майже одночасно була створена Р.У.Флойдом (1967), К.Хоаром (1969) і представниками польської логічної школи (А.Сальвініцький та інші (1970)).
В 1969 році Хоар визначив просту мову програмування через логічну систему аксіом і правила виведення для доведення часткової правильності програми. В його роботі показано, що для визначення семантики мови не в термінах виконання програми, а в термінах доведення її правильності спрощує процес створення програми.
В 70-х роках на базі роботи Хоара починаються дослідження в області аксіомних визначень мови програмування. З’являється багато робіт з аксіоматизації різних конструкцій: від оператора присвоювання до різних форм циклів, від виклику процедур до співпрограм. Головним недоліком дослідників в ті роки було те, що вони не приділяли достатньо уваги формальній логіці.
В 1972 році вийшла чергова стаття Хоара про доказ правильного подання даних, що прискорило дослідження абстрактних типів даних. В СРСР роботи в цій області проводились в Новосибірську (А.П.Єршов, В.Н.Агафонов, А.В.Замулин, И.Н.Скопина).
В 1973 році були сформульовані правила доведення правильності для більшості конструкцій мови Паскаль. В 1975 році була побудована автоматична система «верификации для подмножества» мови Паскаль, заснована на аксіомах і правилах виведення. В 1979 році була визначена мова програмування Евкліда, в проект яого з самого початку була закладена ідея аксіоматизації.
В 1976 році вийшла книга Е.Дейкстри «Дисципліна програмування», в якій пропонується метод доведення правильності програми. Суть методу полягає в тому, щоб будувати програму разом з доведенням, причому доведення повинно випереджати побудову програми. Е.Дейкстр визначив для простої мови програмування слабкі передбачення і показав, як їх можна використовувати в якості підрахування для виведення програми. Стало зрозуміло, що користування формалізмом може призвести до побудови програм більш надійним способом.» [3]
Біографія Хоара
Чарльз Ентоні Річард Хоар – британський вчений, який спеціалізується в області інформатики і обчислювальної техніки. Найбільш відомий як винахідник алгоритму «швидкого сортування» (1960), на сьогоднішній день являється найпопулярнішим алгоритмом сортування.
Інші відомі результати його роботи: мова Z специфікацій і паралельна модель взаємодії послідовних процесів (CSP, Communicating Sequential Process). В числі його заслуг – розробка логіки Хоара (Hoare Logic), наукової основи для конструювання коректних програм, які використовуються для визначення і розробки мови програмування. Хоар створив ряд робіт по створенню специфікацій, проектуванню, реалізації та супроводженню програм, які показують важливість наукових результатів для збільшення продуктивності комп’ютерів і підвищення надійності програмного забезпечення.
Народився Чарльз Ентоні Річард Хоар в Коломбо В Шрі-Ланці. Отримав класичну ступінь бакалавра в Університеті Оксфорда (Merton College) в 1956 році. Проходив службу в ВМС Великобританії в 1956-1958 роках. Вивчив російську мову, він навчався комп’ютерному перекладу під керівництвом А.Н.Колмогорова в Московському державному університеті. В 1960 році, через політичну кризу, пов’язану з винищенням розвідувального літака У-2, він залишив Радянський Союз і почав працювати в невеликій компанії по виробництву комп’ютерів Elliott Brothers, де займався реалізацією мови ALGOL60.

Завантажити цю роботу безкоштовно
Пролистати роботу: 1  2  3 



Реферат на тему: Алгоритмічна логіка Хоара

BR.com.ua © 1999-2017 | Реклама на сайті | Умови використання | Зворотній зв'язок