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

Всього в базі: 75850
останнє поновлення: 2016-12-08
за 7 днів додано 17

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

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

 

ПОШУК:   

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

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

цесів (CSP, Communicating Sequential

Process). В числі його заслуг – розробка логіки Хоара (Hoare Logic),

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

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

створив ряд робіт по створенню специфікацій, проектуванню, реалізації та

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

збільшення продуктивності комп’ютерів і підвищення надійності

програмного забезпечення.

 

Народився Чарльз Ентоні Річард Хоар в Коломбо В Шрі-Ланці. Отримав

класичну ступінь бакалавра в Університеті Оксфорда (Merton College) в

1956 році. Проходив службу в ВМС Великобританії в 1956-1958 роках.

Вивчив російську мову, він навчався комп’ютерному перекладу під

керівництвом А.Н.Колмогорова в Московському державному університеті. В

1960 році, через політичну кризу, пов’язану з винищенням розвідувального

літака У-2, він залишив Радянський Союз і почав працювати в невеликій

компанії по виробництву комп’ютерів Elliott Brothers, де займався

реалізацією мови ALGOL60. Там він закінчив займатися розробкою

алгоритмів. В 1968 році став професором інформатики та обчислювальної

техніки в Королівському Університеті Белфаста (Queen’s University

Belfast). В 1977 році повернувся в Оксфорд, як професор обчислювальної

техніки, щоб очолити дослідницьку групу Programming Research Group, в

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

державних структур, працюючих в області ІТ-індустрії. Тематика його

винахідницької роботи в Оксфорді: коректність програмних специфікацій,

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

вийшов на пенсію в званні почесного професора та перейшов на посаду

головного досліджувача в Microsoft Research в Кембриджі, де і працює по

сьогоднішній день.

 

В 1980 році він отримав Приз Тюрінга за « його видатні досягнення в

визначенні і дизайні мови програмування». В 2000 році йому було

присвоєно звання рицарського титулу за заслуги в області освіти та

комп’ютерних наук, Премії Кіото. [1], [2]

 

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

 

Основою для логіки виведення правильних програм служать аксіоми Хоара.

Вони допускають інтерпретації в термінах програмних конструкцій.

 

Ћ

 

 

ё

 

Ћ

 

ђ

 

ё

 

-

 

R

 

????ё

 

-

 

 

F

 

H

 

J

 

L

 

¬

 

®

 

М

 

О

 

ф

 

ц

 

ш

 

ъ

 

jy

 

R

 

????Сформулюємо аксіоми Хоара, які визначають передумови як достатні

умови, які гарантують, що виконання відповідних операторів при вдалому

завершенні приведе до бажаних після умов. [3]

 

А1. Аксіома присвоювання:

 

істинне перед виконанням.

 

 

 

.

 

 

Аксіома А5 відповідає інтерпретації умовного оператора в мові

програмування.

 

Сформулюємо правило для альтернативного оператора (повна форма умовного

оператора):

 

 

і для операторів циклу.

 

Передумови та після умови циклу until (до) задовольняють правило:

 

 

спочатку.

 

Передумови і після умови циклу while (поки) задовольняють правило:

 

 

Аксіоми А1 – А8 можна використовувати для перевірки узгодження передачі

даних від оператора до оператора, для аналізу структурних властивостей

-----> Page:

[0] 1 [2]

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