Вам бонус- начислено 1 монета за дневную активность. Сейчас у вас 1 монета

Логика в информатике

Лекция



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

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

  • Теоретические основы и анализ
  • Использование компьютерных технологий в помощь логикам
  • Использование концепций из логики для компьютерных приложений

Логика в информатике

Логика в информатике

Схематическое изображение логических операций компьютера

Теоретические основы и анализ

Логика играет фундаментальную роль в информатике. Некоторые из ключевых областей логики, которые имеют особое значение, - это теория вычислимости (ранее называемая теорией рекурсии), модальная логика и теория категорий . Теория вычислений основана на концепциях , определенных логиков и математиков , таких как Алонзо Церкви и Алан Тьюринг . Черч впервые показал существование алгоритмически неразрешимых проблем, используя свое понятие лямбда-определимости. Тьюринг дал первый убедительный анализ того, что можно назвать механической процедурой, а Курт Гедель утверждал, что он нашел анализ Тьюринга «совершенным» Кроме того, некоторые другие основные области теоретического пересечения логики и информатики:

  • Теорема Геделя о неполноте доказывает, что любая логическая система, достаточно мощная, чтобы характеризовать арифметику, будет содержать утверждения, которые нельзя ни доказать, ни опровергнуть в рамках этой системы. Это имеет прямое приложение к теоретическим вопросам, касающимся возможности доказательства полноты и правильности программного обеспечения.
  • Проблема фрейма - это основная проблема, которую необходимо преодолеть при использовании логики первого порядка для представления целей и состояния агента искусственного интеллекта.
  • Соответствие Карри – Ховарда - это связь между логическими системами и программным обеспечением. Эта теория установила точное соответствие между доказательствами и программами. В частности, он показал, что термины в простом типизированном лямбда-исчислении соответствуют доказательствам интуиционистской логики высказываний.
  • Теория категорий представляет собой взгляд на математику, который подчеркивает отношения между структурами. Он тесно связан со многими аспектами информатики: системами типов для языков программирования, теорией систем переходов, моделями языков программирования и теорией семантики языков программирования.

Компьютеры в помощь логикам

Одним из первых приложений, в которых использовался термин « искусственный интеллект», была система Logic Theorist, разработанная Алленом Ньюэллом , Дж. К. Шоу и Гербертом Саймоном в 1956 году. Одна из вещей, которые делает логик, - это взять набор логических утверждений и вывести их выводы (дополнительные утверждения), которые должны соответствовать законам логики. Например, если дана логическая система, которая гласит: «Все люди смертны» и «Сократ - человек», правильным выводом будет «Сократ смертен». Конечно, это банальный пример. В реальных логических системах утверждения могут быть многочисленными и сложными. С самого начала стало понятно, что этому виду анализа может значительно помочь использование компьютеров. Теоретик логики подтвердил теоретические работыБертран Рассел и Альфред Норт Уайтхед в их влиятельной работе по математической логике под названием Principia Mathematica . Кроме того, логики использовали последующие системы для проверки и открытия новых логических теорем и доказательств.

Логические применения для компьютеров

Математическая логика всегда оказывала сильное влияние на область искусственного интеллекта (ИИ). С самого начала работы в этой области было понятно, что технология автоматизации логических выводов может иметь большой потенциал для решения проблем и вывода выводов из фактов. Рон Брахман описал логику первого порядка (FOL) как метрику, с помощью которой все представления знаний ИИформализмы должны быть оценены. Нет более общего или мощного известного метода описания и анализа информации, чем FOL. Причина, по которой FOL просто не используется в качестве компьютерного языка, заключается в том, что он на самом деле слишком выразителен в том смысле, что FOL может легко выражать утверждения, которые ни один компьютер, независимо от его мощности, никогда не сможет решить. По этой причине каждая форма представления знаний в некотором смысле является компромиссом между выразительностью и вычислимостью. Чем выразительнее язык, чем он ближе к FOL, тем больше вероятность того, что он будет медленнее и склонен к бесконечному циклу.

Например, правила ЕСЛИ ТО, используемые в экспертных системах, соответствуют очень ограниченному подмножеству ВОЛС. Вместо произвольных формул с полным набором логических операторов отправной точкой является просто то, что логики называют modus ponens . В результате системы на основе правил могут поддерживать высокопроизводительные вычисления, особенно если они используют преимущества алгоритмов оптимизации и компиляции.

Другой важной областью исследований логической теории была программная инженерия. В исследовательских проектах, таких как программы Knowledge Based Software Assistant и Programmer's Apprentice, применялась логическая теория для проверки правильности спецификаций программного обеспечения. Они также использовали их для преобразования спецификаций в эффективный код на различных платформах и для доказательства эквивалентности реализации и спецификации. [10] Этот формальный подход, основанный на преобразовании, часто требует гораздо больше усилий, чем традиционная разработка программного обеспечения. Однако в определенных областях с соответствующими формализмами и шаблонами многократного использования этот подход оказался жизнеспособным для коммерческих продуктов. Подходящими областями обычно являются такие, как системы вооружений, системы безопасности и финансовые системы в реальном времени, где отказ системы имеет чрезмерно высокие человеческие или финансовые затраты. Примером такой области является очень крупномасштабная интегрированная (СБИС).дизайн - процесс проектирования микросхем, используемых для процессоров и других важных компонентов цифровых устройств. Ошибка в микросхеме - это катастрофа. В отличие от программного обеспечения, микросхемы не подлежат исправлению или обновлению. В результате существует коммерческое обоснование использования формальных методов для доказательства того, что реализация соответствует спецификации.

Еще одно важное применение логики в компьютерных технологиях было в области языков фреймов и автоматических классификаторов. Языки фреймов, такие как KL-ONEимеют жесткую семантику. Определения в KL-ONE можно напрямую сопоставить с теорией множеств и исчислением предикатов. Это позволяет специализированным средствам доказательства теорем, называемым классификаторами, анализировать различные объявления между наборами, подмножествами и отношениями в данной модели. Таким образом, модель может быть проверена и отмечены любые несогласованные определения. Классификатор также может выводить новую информацию, например определять новые наборы на основе существующей информации и изменять определение существующих наборов на основе новых данных. Уровень гибкости идеален для работы в постоянно меняющемся мире Интернета. Технология классификатора построена на основе таких языков, как язык веб-онтологий, чтобы обеспечить логический семантический уровень существующего Интернета. Этот слой называется семантической сетью .

Временная логика используется для рассуждений в параллельных системах .

Включаются следующие основные применения:

  • исследования в логике, вызванные развитием компьютерных наук. Например, аппликативного вычислительные системы, теория вычислений и модели вычислений;
  • формальные методы и логика рассуждения о понятии. Например, семантическая сеть , семантическая паутина ;
  • булева логика и алгебра для разработки аппаратного обеспечения компьютеров;
  • решение задач и структурное программирование для разработки приложений и создания сложных систем программного обеспечения
  • доказательное программирование - технология разработки алгоритмов и программ с доказательствами правильности алгоритмов;
  • фундаментальные понятия и представления для компьютерных наук, которые являются естественной областью для формальной логики. Например, семантика языков программирования ;
  • логика знаний и предположений. Например, искусственный интеллект ;
  • речь Пролог и логическое программирование для создания баз знаний и экспертных систем и исследований в области искусственного интеллекта;
  • логика для описания пространственного положения и перемещения;
  • логика в информационных технологиях. Например, реляционная модель данных , реляционные СУБД , реляционная алгебра , реляционное исчисление ;
  • логика вычислений с объектами. Например, комбинаторная логика, суперкомбинаторы ;
  • логика для компилирования кода и его оптимизации. Например, категориальная абстрактная машина ;
  • логика для эквивалентного преобразования объектов. Например, лямбда-исчисления ;
  • перевикладом логики и математики в терминах, понятных специалистам в компьютерных науках .

Эффективность в компьютерных науках

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

Тестирование программ может обнаружить наличие ошибок в программах, но не может гарантировать их отсутствие. Гарантии отсутствия ошибок в алгоритмах и программах могут дать только доказательства их правильности. Алгоритм не содержит ошибок, если он дает правильные решения для всех допустимых данных.

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

Единственный путь для преодоления этих проблем это изучение систематических методов составления алгоритмов и программ с одновременным анализом их правильности в рамках доказательного программирования с самого начала обучения основам алгоритмизации и программирования.

Сложность для преподавателей и программистов заключается в том, что они должны уметь писать не только алгоритмы и программы, но и доказательства правильности своих алгоритмов и программ. Об этом говорит сайт https://intellect.icu . К сожалению, сейчас это не умеют делать ни математики, ни программисты.

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

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

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

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

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

Чтобы компьютер работал, он должен быть оснащен программным обеспечением, то есть комплексом программ, ориентирующих компьютер на решение задач того или иного класса. Слово «программа» имеет греческое происхождение и означает «объявление», «распоряжение». Уже само понятие компьютерной программы, предусматривающей четкое алгоритмический предписание компьютера о порядке и характер действий, предполагает проникновение в программу, а также в процесс ее сборки (в программирование) теории алгоритмов.

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

Фундаментальная основа программирования

Теория алгоритмов и математическая логика - фундаментальная основа программирования. В 30-е гг. XIX в. английский математик Чарльз Бэббидж впервые высказал идею вычислительной машины. И только сто лет спустя логики разработали четыре математически эквивалентны модели понятия алгоритма. Именно в теории алгоритмов были предусмотреть основные концепции, которые легли в основу принципов построения и функционирования вычислительной машины с программным управлением и принципов создания языков программирования. Идею такой вычислительной машины впервые смогли реализовать болгарский ученый С. Атанасов в 1940 г.. И немецкий ученый К. Цузе в 1942 г.. Четыре главные модели алгоритма породили различные направления в программировании.

Модели понятие алгоритма

  • Первая модель - это абстрактная вычислительная машина ( Тьюринг, Р. Пост). Она появилась абстрактным прообразом реальных вычислительных машин. До сих пор все вычислительные машины в некотором смысле базируются на идее Тьюринга: их память физически состоит из битов, каждый из которых содержит либо 0, либо 1. Программное управление унаследовало от этих абстрактных машин и программу, помещенную в «постоянную память» ( идея поместить программу ЭВМ в основную память, чтобы иметь возможность изменять ее в ходе вычислений, принадлежит Джону фон Нейманом), а структура команды современной ЭВМ в значительной степени напоминает структуру команды машины Тьюринга. В рамках теории машин Тьюринга выкристаллизовались важнейшие для компьютерных приложений логики понятия: Ориентировочная функция, выполнимая задача, неразрешимая (алгоритмически) задача. Собрано большое количество определений абстрактных вычислительных машин и показано,
  • Вторая модель - это рекурсивные функции, идея которых восходит к гильбертивського аксиоматического подхода. От них унаследовало свои основные конструкции современное структурное программирование.
  • Третий способ описания алгоритмов - нормальные алгоритмы А. А. Маркова . Они послужили основой языка Рефал и многих других языков обработки символьной информации.
  • Четвертое направление в теории алгоритмов - так называемое λ-исчисление - базируется на идеях советского логика Г. Шейнфинкель и американского логика Карри, Хаскелл . Оказалось, что для определения всех вычислительных функций достаточно операций так называемой λ - абстракции и суперпозиции. Идеи λ -Многочисленные активно развиваются в языке Лисп, функциональном программировании и во многих других перспективных направлениях современного программирования.

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

Описание компьютерных программ с помощью математической логики

Первые попытки применить в программировании развитые логические исчисления и методы формализации сделал американский логик Г. Б. Карри. В 1952 г.. Он сделал доклад «Логика программных композиций», идеи которой опередили свое время как минимум на четверть века. Карри рассмотрел задачу программирования, как задача составления больших программ из готовых кусков. Были введены две базовые системы конструкций: первая - последовательное выполнение, ветвление и цикл, вторая - последовательное выполнение и условный переход. Он охарактеризовал логические средства, которые можно использовать для композиции программ из подпрограмм в каждом из этих случаев.

Как известно, компьютер является своего рода «идеальным бюрократом»: он не воспримет программу, написанную на не до конца формализованной языке, и приступит к работе только после того, как все выражено в полном соответствии с подробными инструкциями. Поэтому в 1960-е гг. На первый план вышли задачи точного определения формальных языков достаточно сложной структуры. Математическая логика, поддерживаемая идеями программирования, успешно с ними справилась, разработали описание синтаксиса сложных и богатых выразительными средствами формальных языков.

В середине 1960-х гг. Практически одновременно появился ряд пионерских работ в области описания условий, которым удовлетворяет программа. Советский математик В. М. Глушков в 1965 г.. Ввел понятие алгоритмической алгебры, послужило прообразом алгоритмических логик. Ф. Енгелер в 1967 г.. Предложил использовать языка с бесконечно длинными формулами, чтобы выразить бесконечное множество возможностей, возникающих при различных исполнениях программы. Но наибольшую известность приобрели языка алгоритмических логик. Эти языки были изобретены практически одновременно американскими логиками Г. В. Флойдом (1967), С. А. Г. Гоар (1969) и учеными польской логической школы, например А. Сальвицким (1970) и др.

Алгоритмическая логика (или динамическая логика, или программная логика, или логика Гоара ) - раздел теоретического программирования, в рамках которого исследуются аксиоматические системы, представляющие средства для задания синтаксиса и семантики языков программирования, а также для синтеза компьютерных программ и их верификации ( проверки правильности работы). Языки алгоритмических логик основываются на логике предикатов 1-го порядка и включают в себя высказывания вида {A} S {B}, читаются следующим образом: «Если к выполнению оператора S было выполнено A, то после него будет выполнено B». Здесь A называется предпосылкой, B - постусловием, или обещанием S. На этом языке даются логические описание операторов присвоения и условного перехода, ветвления, цикла.

Наряду с динамической логике 1-го порядка рассматривается пропозициональные динамическая логика и ее обобщения - так называемая логика процессов, в которой выражены некоторые свойства программы, зависящие от процесса ее выполнения. Различные динамические логики получаются при варьировании средств языков программирования, используемых в программах. Эти средства содержат массивы и другие структуры данных, рекурсивные процедуры, циклические конструкции, а также средства задания недетерминированных программ.

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

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

Принципиально другой способ определения семантики программ, пригодный, скорее для описания всей алгоритмического языка, а не конкретных программ, предложил в 1970 г.. Американский логик Д. Скотт. Он построил математическую модель λ-исчисление и показал, как переводить функциональное описание языка структурного программирования в λ-исчисление и как определить математическую модель алгоритмического языка через модель λ-исчисление. Эта так называемая денотацийна семантика алгоритмических языков, стала практическим инструментом построения надежных трансляторов из сложных алгоритмических языков. Так еще один абстрактная область математической логики нашла прямые практические применения.

Описание программирования и анализ его концепций с помощью математической логики

Программирование - это процесс составления программы, плана действий. Было отмечено, что классическая логика плохо подходит для описания этого процесса хотя бы потому, что она плохо подходит вообще для описания всякого процесса в математике. Еще в начале XX в. стало ясно, что в математике давно разошлись понятие «существовать» и «быть построенным», которые с античных времен трактовались как синонимы. Были обнаружены так называемые математические объекты - «привидения» (множества, функции, числа), существование которых доказано, но построить что можно. Причиной их появления появился эффект сочетания классической логики теореме Геделя о неполноте формальной арифметики. Один из фундаментальных законов классической логики - закон исключенного третьего (P ˅ ˥P) в некотором свободной трактовке фактически означает, что мы знаем. Этот постулат конечно же никак нельзя назвать реалистичным: мы знаем очень мало, и чем больше узнаем, тем лучше это понимаем. голландский математикЛ. Э. Я. Брауэр определил логические корни «призраков», еще до открытия теоремы Геделя, в 1908 г.., И начал построение так называемой интуитивной математики, не принимает закон (P ˅ ˥P), как универсальный. В 1930-1932 гг. Второй голландец А. Гейтинг строго сформулировал логику, которой пользовались в интуитивной математике - интуитивную логику. Ее математическая интерпретация, изложенная советским математиком А. Н. Колмогоровым сохранила свое значение до сих пор.

А. Н. Колмогоров рассмотрел логику как исчисления задач. Каждая формула алгебры высказываний рассматривается не просто как формула, а как требование решить задачу, то есть построить объект, удовлетворяющий некоторым условиям. Это так называемая конструктивная интерпретация логики высказываний. Логические связи понимаются как средства построения формулировок более сложных задач с простых, аксиомы - как задачи, решение которых дано, правила вывода - как способы преобразования решений одних задач в решение других. Отметим, что решение задачи - это не только сам искомый объект, но и доказательство того, что он удовлетворяет предъявляемым требованиям. Например, формула A B понимается в колмогоривський интерпретации как задача, заключается в том, чтобы построить решение задачи A и решение задачи B, правило вывода A, B \ A B - как преобразования,а , решение задачи A, и объекта b , решение задачи B, пару ( a, b ), решение задачи A B. Объект a , решает задачи, сопоставлено формуле A, называется реализацией A. Этот факт сказывается a RA. Центральным моментом конструктивного понимания логических формул является интерпретация импликации. Конструктивная импликация A → B понимается, как требование построить эффективное преобразование f, примененное ко всем реализаций формулы A и переводит их в реализации формулы B.

Нечеткое колмогоривське формулировки логики, как вычисления задач, породила многочисленные различные конкретизации, дав целую систему точных математических определений. Эта формулировка нашло применение не только в интуитивной логике, для которой она была создана, но и в других логических системах. Строгие математические семантики, основанные на идее Колмогорова, обычно называют семантиками реализуемости (в отличие от других видов логических семантик, основанные на системах истинностных значений). Первую реализуемость построил американский логик С. К. Клини в 1940 г.. Для арифметики с интуитивной логикой. В 1960-1980-х гг. Появились десятки понятий реализуемости, как для систем, основанных на интуитивной логике, так и для других логик. Советский логик А. А. Воронков в 1985 г.. Вывел условия, при которых классическая логика может рассматриваться как конструктивное. Из них, в частности, следует, что необходимым (но не достаточным) условием конструктивности классической теории является ее полнота, то есть выводимость в ней для каждой замкнутой формулы F или самой F, или ее отрицание ˥F. Тем самым еще раз подтвердилось прозрение Брауэра по логических корней неконструктивности. Заметим, что примерами классических теорий, имеющих конструктивное толкование, служат элементарная геометрия и алгебраическая теория действительных чисел.

Описание программирования с помощью логики основано на определенной аналогии между выводом формулы в некотором логическом исчислении и программой решения задачи, соответствует этой формуле при конструктивной интерпретации логики. Логическая теория, соответствующая структурным схемам программ, появилась в середине 1980-х гг. Структурные схемы отвечали нарождающемуся новому типу логики - логики схем программ, которой пользуется программист для создания сложных, многовариантных, итеративных планов действий.

Верификация программ с помощью математической логики

Широкое использование компьютеров в различных сферах человеческой деятельности ставит вопрос надежности программного обеспечения компьютеров. Как известно, правильность созданной программы обычно проверяется на ряде так называемых тестовых примеров, на начальных данных, для которых результат известен или его можно предвидеть. Нетрудно понять, что такая проверка способна только выявить наличие ошибок в программе, но не довести их отсутствие.

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

С интуитивной точки зрения программа будет правильной, если в результате ее выполнения будет достигнут тот результат, с целью получения которого и была написана программа. Доказательство правильности программы заключается в предъявлении такой цепочки аргументов, убедительно свидетельствуют о том, что это действительно так, то есть, что программа на самом деле решает поставленную задачу.

Сформулируем теперь точное определение понятия правильности программы. Пусть α - программа, P - утверждение, что относится к входным данным, которое должно быть истинно перед выполнением программы α (оно называется условием программы α), Q - утверждение, которое должно быть истинно после выполнения программы α (оно называется постусловием программы α) . Различают два вида правильности программ: частичную и тотальную (полное). Программа α называется частично правильной по предпосылки P и постусловия Q, если каждый раз, когда перед выполнением α предпосылка P истинная для входных значений переменных, и α завершает работу, Постусловия Q также будет истинной для исходных значений переменных. В этом случае будем использовать запись P [α] Q. Программа α называется тотально правильной относительно P и Q, если она частично правильная относительно P и Q, и α обязанности " обязательно завершает свою работу для входных значений переменных, удовлетворяющих условию P. В этом случае пишем P [α! ] Q.

Обратим внимание на то, что понятие правильности программы α сформулировано по соответствующим утверждений (условий) P и Q. Поэтому из истинности утверждения P [α] Q (или P [α!] Q соответственно) не обязательно следует истинность утверждения о правильности программы при других предпосылках и Постусловия. Аналогичным образом, замена в P [α] Q (или P [α!] Q) программы α на программу β, вообще говоря, не сохраняет истинностного значения утверждение о правильности. Не следует также думать, что при данных условиях P и Q существует только одна программа α, для которой высказывания P [α] Q (или P [α!] Q) истинно.

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

Из определений следует, что всякая тотально правильная программа является частично правильной при тех же предпосылках и Постусловия. Обратное конечно же неверно. Понятно, что тотальная правильность «лучшая» за частичную, хотя доказать тотальную правильность программы, пожалуй, сложнее, чем частичную.

Для доказательства частичной правильности операторных программ обычно используются различные модификации метода Флойда, который заключается в следующем. На схеме программы выбираются контрольные точки так, чтобы любой циклический путь проходил по крайней мере через одну точку. С каждой контрольной точкой ассоциируется специальное условие (индуктивное утверждение или инвариант цикла), истинная при каждом переходе через эту точку. С входом и выходом схемы также ассоциируются пред- и постусловия. Затем каждому пути программы между двумя соседними контрольными точками сопоставляется так называемая условие правильности. Выполнимость всех условий правильности гарантирует частичную правильность программы.

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

Одна из модификаций метода Флойда заключается в построении конечной аксиоматической системы (так называемой «логики Гоара» ), состоящий из схем аксиом и правил вывода, в которой как теоремы выводятся утверждения о частичной правильности программ, в частности на языке программирования Паскаль. Такая система используется и для задания аксиоматической семантики языка Паскаль. Аксиоматические системы, родственные логике Гоара, разработаны и для других алгоритмических языков программирования.

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

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

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

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

Логическое описание семантики программы:

1) если i и j — это вход и выход операторной вершины, то переход из i в j — это дуга,

которая определяется импликацией Qi(t1, t2, tn) —> Q;(l1,l2, ..ln), где li = f(t1 ..., tn) обозначение соответствующего преобразова

ния, выполняемого оператором;

  • 2 ) если i и j — вход и выход условной вершины, то дуге «i —> ставится в соответствие формула с контрольным предикатом Qi & Р —> Qi, где Р = P(t1, ..., tn) контрольный предикат;
  • 3) узел Qm объединяет два и более состояний Qi, на входе операторной или условной вершины и записывается в виде тождества Qm = ΣQi(ti, t2,... ,tn),
  • 4) начало программы Q0 — нуль-местный предикат (простое высказывание);
  • 5) конец программы — Qk.

Для целого умножения используется очевидный простой алгоритм многократного суммирования Логика в информатике .

Для описания алгоритма используется блок-схема, в которой А, В — целые числа; А — множимое; В — множитель; S — произведение, которое вычисляется по указанной формуле (рис. 5.2).

Логика в информатике

Рис. 5.2. Схема алгоритма к примеру 5.3

Формулы, описывающие схему алгоритма, в которой выделены точки контроля состояния машины Qq, ..., Q6):

Логика в информатике

Контрольные формулы-инварианты в алгоритме:

Логика в информатике

Интерпретация формул для конкретных исходных данных эквивалентна исполнению программы.

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

Q6(А, В, S) && (В = 0), т.е.

Логика в информатике

Исполнение программы состоит из следующих шагов:

1) подстановка (интерпретация) значений переменных после ввода данных в формулу:

Логика в информатике

  • 2) переход к следующей формуле, в которой условие импликации истинно, и запуск итерационного процесса интерпретации (Q1 = Т):
    • а) выполнение формул, пока Fi+1 не равно Fi,
    • б) формулы можно упорядочить для ускорения итерации;
    • в) формулы можно интерпретировать параллельно.

Символическое тестирование и частичные вычисления используются

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

Зададимся множимым А = а и множителем В = 3.

Интерпретация алгоритма в логике предикатов:

Логика в информатике

Подтверждается исполнение формулы S =а • 3 = Σ= a + a + а.

В традиционном программировании используются контрольные формулы, в которых проверяется состояние данных в конкретных точках программы. В языках программирования таких как C++ используется оператор assert (логическая формула с предикатами), при интерпретации этой формулы формируется признак (F или T), который позволяет контролировать возможные ошибки в исходных данных и вычислениях.

Вау!! 😲 Ты еще не читал? Это зря!

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

Ответы на вопросы для самопроверки пишите в комментариях, мы проверим, или же задавайте свой вопрос по данной теме.

создано: 2023-05-18
обновлено: 2023-05-18
132265



Рейтиг 9 of 10. count vote: 2
Вы довольны ?:


Поделиться:

Найди готовое или заработай

С нашими удобными сервисами без комиссии*

Как это работает? | Узнать цену?

Найти исполнителя
$0 / весь год.
  • У вас есть задание, но нет времени его делать
  • Вы хотите найти профессионала для выплнения задания
  • Возможно примерение функции гаранта на сделку
  • Приорететная поддержка
  • идеально подходит для студентов, у которых нет времени для решения заданий
Готовое решение
$0 / весь год.
  • Вы можите продать(исполнителем) или купить(заказчиком) готовое решение
  • Вам предоставят готовое решение
  • Будет предоставлено в минимальные сроки т.к. задание уже готовое
  • Вы получите базовую гарантию 8 дней
  • Вы можете заработать на материалах
  • подходит как для студентов так и для преподавателей
Я исполнитель
$0 / весь год.
  • Вы профессионал своего дела
  • У вас есть опыт и желание зарабатывать
  • Вы хотите помочь в решении задач или написании работ
  • Возможно примерение функции гаранта на сделку
  • подходит для опытных студентов так и для преподавателей



Комментарии


Оставить комментарий
Если у вас есть какое-либо предложение, идея, благодарность или комментарий, не стесняйтесь писать. Мы очень ценим отзывы и рады услышать ваше мнение.
To reply

Разработка программного обеспечения и информационных систем

Термины: Разработка программного обеспечения и информационных систем