Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АрхитектураБиологияГеографияДругоеИностранные языки
ИнформатикаИсторияКультураЛитератураМатематика
МедицинаМеханикаОбразованиеОхрана трудаПедагогика
ПолитикаПравоПрограммированиеПсихологияРелигия
СоциологияСпортСтроительствоФизикаФилософия
ФинансыХимияЭкологияЭкономикаЭлектроника

Понятие об алгоритмической логике Ч. Хоара.



Читайте также:
  1. I. Понятие о бинере и его роль в метафизике
  2. II. О трансцендентальной логике
  3. А.Н. Леонтьев вводит понятие ведущая деятельность. Она является движущей силой развития.
  4. Акционерное общество: понятие и признаки, виды.
  5. Ассоциация как механизм работы сознания. Понятие апперцепции
  6. Б. Понятие о классической статистике. Скорости молекул. Распределение молекул по скоростям и энергиям. Барометрическая формула
  7. Бланковые, опросные, рисуночные и проективные психодиагностические методики. Сущность и частота встречаемости. Понятие об объективно-манипуляционных методиках

Язык алгоритмических логик сочетает язык описания программ и логический язык, что дает возможность выражать разнообразные свойства программ. Это программная или динамическая логика.

Применяется для описания свойств частичной корректности программ. Использует выражения:

(исходное состояние памяти) (программа заканчивает работу) (заключительное состояние памяти)

 

где P, Q – логические формулы, а A – программа.

Такая формула имеет следующий смысл: Если исходное состояние памяти (исходное значение переменных удовлетворяет условию P и программа A завершает работу над , то заключительное значение переменных удовлетворяет условию Q.

Верификация – доказательство правильности программ. Алгоритмическая логика позволяет доказать правильность (неправильность) программ без перебора всевозможных вариантов их реализации на различных сочетаниях переменных.

В [1] приводятся примеры языков алгоритмических логик, использующих высказывания вида:

{U}S{В} – «Если до исполнения оператора S будет выполнено U, то после него будет В». Здесь U – предусловие, а В – постусловие. При анализе условных операторов программы, если ни при каких вариантах не реализуется один из его выходов – фиксируется ошибка. При описании циклов, что является наиболее трудным, анализируются возможности выходов из них. Каждое состояние памяти, возникающее в ходе исполнения программы, – «возможный мир». Пути исполнения программы – переходы между «мирами». В случае тотальной корректности программа обязательно завершается: ^B. Частичная корректность:

Автоматическое доказательство правильности программ – задача до сих пор нерешенная.


Дата добавления: 2015-07-11; просмотров: 137 | Нарушение авторских прав






mybiblioteka.su - 2015-2024 год. (0.007 сек.)