Математическая логика и теория алгоритмов


Предикатные временные логики



страница5/5
Дата05.05.2018
Размер63.5 Kb.
ТипЛекция
1   2   3   4   5
Предикатные временные логики ______________________________________________________

_____________________________________________________________________________________

При этом описание программы состоит в выражении с помощью языка временной логики свойств программы, характеризующих ее правильное вычислительное поведение, а ее верификация в использовании аппарата временного исчисления для доказательства того, что данная программа обладает интересующим свойством.

Программы рассматриваются как объекты, выраженные на формальном языке, обладающие определенной информационной и логической структурой и подлежащие исполнению на автоматических устройствах. Исследование программ проводится преимущественно на основе двух моделей вычислений: последовательных программ с памятью, или операторных программ, и рекурсивных программ.

Определение класса программ слагается из трех частей: схемы программы (синтаксиса), интерпретации и семантики. Схема программы — это конструктивный объект, показывающий, как строится программа с использованием сигнатурных символов. Интерпретация – это задание конкретного носителя и сопоставление символам сигнатуры конкретных операций и отношений на носителе. Семантика — это способ сопоставления каждой программе результата ее выполнения. Как правило, с программами связывают вычисляемые ими функции. Интерпретация обычно входит в семантику как параметр, поэтому схема программы задает множество программ и вычисляемых ими функций, которое получается при варьировании интерпретаций над некоторым запасом базовых операций.


Алгоритмические логики _____________________________________________________________

_______________________________________________________________________________________________________________________________________________________________________________________________________________________________________________________________

Эти логики были изобретены Р. У. Флойдом (1967г.), Ч. Хоаром (1969г.) и представителями польской логической школы (А. Сальвиницкий и др. (1970 г.)).

Хоар определил простой язык программирования через логическую систему аксиом и правил вывода для доказательства частичной правильности программ. Им показано, что определение семантики языка не в терминах выполнения программы, а в терминах доказательства ее правильности упрощает процесс построения программы.

На базе работы Хоара проводились исследования в области аксиоматических определений языков программирования. Появилось много работ по аксиоматизации различных конструкций: от оператора присваивания до различных форм циклов, от вызова процедур до сопрограмм. В 1973г. были сформулированы правила доказательства правильности для большинства конструкций языка Паскаль. В 1975г. была построена автоматическая система верификации для языка Паскаль, основанная на аксиомах и правилах вывода.

В 1976г. Э. Дейкстра предложил метод доказательства правильности программ. Суть метода заключается в том, чтобы строить программу вместе с доказательством, причем доказательство должно опережать построение программы. Дейкстра определил для простого языка программирования слабейшие предусловия и показал, как их можно использовать в качестве исчисления для вывода программ. Стало ясно, что использование формализма может привести к построению программ более надежным способом.



Алгоритмическая логика Хоара является основой для логики выводов правильных программ и допускает интерпретации в терминах программных конструкций. Аксиомы Хоара (или правила верификации), определяют предусловия как достаточные условия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желательным постусловиям.
Каталог: new -> SubjectFGOS
new -> Концепция краевой системы поиска, поддержки и продвижения талантливых детей и молодежи в Красноярском крае на 2016-2020 года
new -> Проблема преображения человека в философии
new -> Программа минимума кандидатского экзамена по специальности
SubjectFGOS -> Глоссарий по социологии Абсолютная бедность
SubjectFGOS -> Лекция первая. Вводная лекция Лекция вторая. Античная философия
SubjectFGOS -> Содержательный блок
SubjectFGOS -> Н. Н. Епифанова физическое воспитание и спортивная игровая деятельность студентов в вузе учебное пособие


Поделитесь с Вашими друзьями:
1   2   3   4   5


База данных защищена авторским правом ©znate.ru 2019
обратиться к администрации

    Главная страница