ТЕОРИЯ ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ. Теория вычислительных процессов
 Скачать 2.17 Mb.
|
|
case<выражение> of <десятичное_число> => Md(<десятичное_число>, s) <переменная> =>if VARMAP(<переменная>, s) = undef then error else VARMAP(<переменная>, s) <двоичное_выражение> => if (Me(<двоичное_выражение>.<выражение_слева>, s) = undef OR Me(<двоичное_выражение>.< выражение_справа >, s) = undef) then error else if (<двоичное_выражение>.< оператор > = '+' then Me(<двоичное_выражение>.<выражение_слева>, s) + Me(<двоичное_выражение>.<выражение_справа>, s) else Me(<двоичное_выражение>.<выражение_слева>, s) × Me(<двоичное_выражение>.<выражение_справа>, s). Оператор присваивания - это вычисление выражения плюс присваивание его значения переменной, находящейся в левой части. Сказанное можно описать следующей функцией: Ма(х = Е, s) if Me(E, s) = error then error else s' = {<i1', v1'>, <i2', v2'>,..., <in', vn'>} where for j = 1, 2, ..., n, vj' = VARMAP(ij', s) if ij <>x; Me(E, s) if ij = x. Отметим, что два сравнения, выполняющиеся в двух последних строках(ij <> x и ij = х), относятся к именам, а не значениям. После определения полной системы для заданного языка ее можно использовать для определения смысла полных программ этого языка. Это создает основу для очень строгого способа мышления в программировании. Денотационная семантика может использоваться для разработки языка. Операторы, описать которые с помощью денотационной семантики трудно, могут оказаться сложными и для понимания пользователями языка, и тогда разработчику следует подумать об альтернативной конструкции. С одной стороны, денотационные описания очень сложны, с другой - они дают великолепный метод краткого описания языка. Декларативная семантика Декларативная семантика является существенной характеристикой языков логического программирования, в которых программы состоят из объявлений (деклараций), а не из операторов присваивания и управляющих операторов. Эти объявления в действительности являются операторами, или высказываниями, в символьной логике. Основная концепция декларативной семантики заключается в том, что существует простой способ определения смысла каждого оператора, и он не зависит от того, как именно этот оператор используется для решения задачи. Декларативная семантика значительно проще, чем семантика императивных (применяющихся в компьютерах с фон-неймановской архитектурой) языков. Она не требует для проверки отдельного оператора рассмотрения его контекста, локальных объявлений или последовательности выполнения программы. Формальное определение семантики становится общепринятой частью определения нового языка. Стандартное описание языка PL/I включает в себя VDL-подобную нотацию, описывающую семантику операторов PL/I, а для языка Ada было разработано определение на основе денотационной семантики. Тем не менее, изучение формальных определений семантики не оказало такого сильного влияния на практическое определение языков, как изучение формальных грамматик — на определение синтаксиса. Ни один из методов определения семантики не оказался по настоящему полезным ни для пользователя, ни для разработчиков компиляторов языков программирования. Языки формальной спецификации Языки и методы формальной спецификации, как средство проектирования и анализа программного обеспечения появились более сорока лет назад. За это время было немало попыток разработать как универсальные, так и специализированные языки формальных спецификаций (ЯФС), которые могли бы стать практическим инструментом разработки программ, таким же, как, например, языки программирования. За свою недолгую историю ЯФС уже прошли через несколько периодов подъема и спада. Оценки перспектив ЯФС варьировались от оптимистических прогнозов, предсказывающих появление языков описания требований, по которым будет генерироваться готовое программное обеспечение, до пессимистических утверждений, что ЯФС всегда будут только игрушкой для экспериментов в академических исследованиях. Вместе с тем, хотя сейчас даже термин «языки формальных спецификаций» известен далеко не всем программистам, нужно констатировать, что в этой отрасли программирования получены значительные результаты. Они выражаются, во-первых, в том, что есть несколько ЯФС, которые уже нельзя назвать экспериментальными, более того, некоторые ЯФС подкреплены соответствующими стандартами. Во-вторых, более четким стало представление о способах использования ЯФС, о месте формальных методов в жизненном цикле разработки программного обеспечения и в процессах его разработки и использования. Второй из перечисленных факторов важен, поскольку способ использования языка, как, оказалось, серьезно влияет на эволюцию языка. Если рассматривать историю языков спецификации общего назначения (универсальных, не специализированных), то видно, что они развивались в соответствии со следующим представлением о «правильном порядке» разработки программного обеспечения: описать эскизную модель (функциональности, поведения); доказать, что модель корректна (не противоречива, консистентна); детализировать (уточнить) модель; доказать, что детализация проведена корректно; повторять два предыдущих шага до тех пор, пока не будет получена готовая программа. Установка на данную схему процесса разработки приводила к акцентированному вниманию на средства обобщенного описания функциональности, средства уточнения, средства аналитического доказательства корректности в стиле традиционных математических доказательств. Как следствие, появились языки, которые не содержали в себе конструкций, затрудняющих аналитические доказательства, при этом они лишались и тех конструкций, без которых трудно описать реализацию сколько-нибудь сложной программной системы. У специализированных языков несколько другая история. Некоторые из них, например SDL (SpecificationandDesignLanguage), родились из практики проектирования систем релейного управления, где проект традиционно был больше похож на чертеж, чем на текстовое (языковое) описание. Здесь эволюция заключалась во взаимном сближении графической и текстовой нотации на основе взаимных компромиссов и ограничений. При этом участниками компромисса была некоторая графическая нотация и языки программирования, опыт, накопленный в других языках формальных спецификаций, либо игнорировался, либо заимствовался с большим опозданием. ЯФС традиционно рассматривались как средство проектирования. Новый взгляд на ЯФС появился, когда стала актуальной задача анализа уже существующего программного обеспечения. Существенное продвижение на этом фронте было связано с направлением Объектно-Ориентированного Анализа. Его идеи во многом созвучны с Объектно-Ориентированным Проектированием. Не удивительно, что оба эти направления предлагают близкие изобразительные средства для описания архитектуры и поведения систем. В последнее время наиболее известным средством такого рода является (преимущественно) графический язык UML (Unified Modelling Language). Заметим, что UML и подобные ему языки спецификации, безусловно, являются неплохими средствами проектирования, но обычно непригодны для доказательства правильности, на что делался акцент в классических языках спецификации. Совершенно новые требования к языкам спецификации появились с идеей использования их как источников для генерации тестов. Оказалось, что разные виды приложений требуют различных подходов к спецификации и имеют непохожие друг на друга возможности для генерации тестов. В частности, одни виды спецификаций в большей степени пригодны для генерации последовательностей тестовых воздействий (цепочек), тогда как другие предоставляют удобные возможности для генерации тестовых оракулов – программ, оценивающих результат, полученный в ответ на тестовое воздействие. Имеется несколько способов классификации подходов к спецификации. Различают моделе-ориентированные и свойство-ориентированные спецификации или спецификации, основанные на описании состояний и действий. Единой классификации не существует, мы рассмотрим следующие четыре класса подходов к спецификации: исполняемые, алгебраические, сценарные и ограничения. Исполнимые спецификации, исполнимые модели. Этот подход предполагает разработку прототипов (моделей) систем для демонстрации возможности достижения поставленной цели и проведения экспериментов при частичной реализации функциональности. Примерами таких методологий и языков являются SDL, RSL (RAISESpecificationLanguage). Алгебраические спецификации предполагают описание свойств композиций операций. Композиции могут быть последовательными, параллельными, с временными ограничениями и без. Преимуществом этого подхода является то, что в идеале можно полностью абстрагироваться от структур данных, которые используются в качестве входных и выходных значений и, возможно, используются для сохранения внутреннего состояния моделей. Основной недостаток – это нетрадиционность приемов спецификации, что затрудняет их внедрение в промышленных разработках. В качестве примера языка алгебраических спецификаций можно назвать ASN1 (Abstract Syntax Notation One), стандарт которого входит в группу стандартов, описывающих SDL, RSL. Сценарные спецификации описывают не непосредственно целевую систему, а способы ее использования или взаимодействия с ней. Оказывается, что такие косвенные описания, с одной стороны, позволяют судить о некоторых свойствах системы (тем самым, они, конечно, являются спецификациями), и, с другой стороны, такие спецификации могут служить хорошим руководством по использованию системы, что не всегда можно сказать о других видах спецификаций. Наибольшее распространение получили работы OMG группы и продукты компании Rational Corporation. Ограничения состоят из пред- и постусловий функций, процедур и других операций и инвариантов данных. Имеются расширения этого подхода для объектно-ориентированных спецификаций. В этом случае к спецификациям операций добавляются спецификации методов классов, а к инвариантам – инварианты объектов и классов. Языком, поддерживающим спецификацию ограничений, является RSL. Верификация программ Методы доказательства правильности программ Как известно, универсальные вычислительные машины могут быть запрограммированы для решения самых разнородных задач - в этом заключается одна из основных их особенностей, имеющая огромную практическую ценность. Один и тот же компьютер, в зависимости от того, какая программа находится у него в памяти, способен осуществлять арифметические вычисления, доказывать теоремы и редактировать тексты, управлять ходом эксперимента и создавать проект автомобиля будущего, играть в шахматы и обучать иностранному языку. Однако успешное решение всех этих и многих других задач возможно лишь при том условии, что компьютерные программы не содержат ошибок, которые способны привести к неверным результатам. Можно сказать, что требование отсутствия ошибок в программном обеспечении совершенно естественно и не нуждается в обосновании. Но как убедиться в том, что ошибки, в самом деле, отсутствуют? Вопрос не так прост, как может показаться на первый взгляд. К неформальным методам доказательства правильности программ относят отладку и тестирование, которые являются необходимой составляющей на всех этапах процесса программирования, хотя и не решают полностью проблемы правильности. Существенные ошибки легко найти, если использовать соответствующие приемы отладки (контрольные распечатки, трассировки). Тестирование – процесс выполнения программы с намерением найти ошибку, а не подтвердить правильность программы. Суть его сводится к следующему. Подлежащую проверке программу неоднократно запускают с теми входными данными, относительно которых результат известен заранее. Затем сравнивают полученный машиной результат с ожидаемым. Если во всех случаях тестирования налицо совпадение этих результатов, появляется некоторая уверенность в том, что и последующие вычисления не приведут к ошибочному итогу, т.е. что исходная программа работает правильно. Мы уже обсуждали понятие правильности программы с точки зрения отсутствия в ней ошибок. С интуитивной точки зрения программа будет правильной, если в результате ее выполнения будет достигнут результат, с целью получения которого и была написана программа. Сам по себе факт безаварийного завершения программы еще ни о чем не говорит: вполне возможно, что программа в действительности делает совсем не то, что было задумано. Ошибки такого рода могут возникать по различным причинам. В дальнейшем мы будем предполагать, что обсуждаемые программы не содержат синтаксических ошибок, поэтому при обосновании их правильности внимание будет обращаться только на содержательную сторону дела, связанную с вопросом о том, достигается ли при помощи данной программы данная конкретная цель. Целью можно считать поиск решения поставленной задачи, а программу рассматривать как способ ее решения. Программа будет правильной, если она решит сформулированную задачу. Метод установления правильности программ при помощи строгих средств известен как верификация программ. В отличие от тестирования программ, где анализируются свойства отдельных процессов выполнения программы, верификация имеет дело со свойствами программ. В основе метода верификации лежит предположение о том, что существует программная документация, соответствие которой требуется доказать. Документация должна содержать: спецификацию ввода-вывода (описание данных, не зависящих от процесса обработки); свойства отношений между элементами векторов состояний в выбранных точках программы; спецификации и свойства структурных подкомпонентов программы; спецификацию структур данных, зависящих от процесса обработки. К такому методу доказательства правильности программ относится метод индуктивных высказываний, независимо сформулированный К. Флойдом и П. Науром. Суть этого метода состоит в следующем: 1) формулируются входное и выходное высказывания: входное высказывание описывает все необходимые входные условия для программы (или программного фрагмента), выходное высказывание описывает ожидаемый результат; 2) предполагая истинным входное высказывание, строится промежуточное высказывание, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным высказываниями); такое высказывание называется выведенным высказыванием; 3) формулируется теорема (условия верификации): из выведенного высказывания следует выходное высказывание; 4) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента). Доказательство проводится при помощи хорошо разработанных математических методов, использующих исчисление предикатов первого порядка. Условия верификации можно построить и в обратном направлении, т.е., считая истинным выходное высказывание, получить входное высказывание и доказывать теорему: из входного высказывания следует выведенное высказывание. Такой метод построения условий верификации моделирует выполнение программы в обратном направлении. Другими словами, условия верификации должны отвечать на такой вопрос: если некоторое высказывание истинно после выполнения оператора программы, то, какое высказывание должно быть истинным перед оператором? Построение индуктивных высказываний помогает формализовать интуитивные представления о логике программы. Оно и является самым сложным в процессе доказательства правильности программы. Это объясняется, во-первых, тем, что необходимо описать все содержательные условия, и, во-вторых, тем, что необходимо аксиоматическое описание семантики языка программирования. Важным шагом в процессе доказательства является доказательство завершения выполнения программы, для чего бывает достаточно неформальных рассуждений. Таким образом, алгоритм доказательства правильности программы методом индуктивных высказываний представляется в следующем виде: 1) Построить структуру программы. 2) Выписать входное и выходное высказывания. 3) Сформулировать для всех циклов индуктивные высказывания. 4) Составить список выделенных путей. 5) Построить условия верификации. 6) Доказать условие верификации. 7) Доказать, что выполнение программы закончится. Этот метод сравним с обычным процессом чтения текста программы (метод сквозного контроля). Различие заключается в степени формализации. Преимущество верификации состоит в том, что процесс доказательства настолько формализуем, что он может выполняться на вычислительной машине. В этом направлении в восьмидесятые годы проводились исследования, даже создавались автоматизированные диалоговые системы, но они не нашли практического применения. Для автоматизированной диалоговой системы программист должен задать индуктивные высказывания на языке исчисления предикатов. Синтаксис и семантика языка программирования должны храниться в системе в виде аксиом на языке исчисления предикатов. Система должна определять пути в программе и строить условия верификации. Основной компонент доказывающей системы - это построитель условий верификации, содержащий операции манипулирования предикатами, алгоритмы интерпретации операторов программы. Вторым компонентом системы является подсистема доказательства теорем. Отметим трудности, связанные с методом индуктивных высказываний. Повторим, что трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства высказываний о программах». Вторая трудность - семантическая, заключающаяся в формировании самих высказываний, подлежащих доказательству. Если задача, для которой пишется программа, не имеет строгого математического описания, то для нее сложнее сформулировать условия верификации. Перечисленные методы имеют одно общее свойство: они рассматривают программу как уже существующий объект и затем доказывают ее правильность. Метод, который сформулировали К. Хоар и Э. Дейкстра основан на формальном выводе программ из математической постановки задачи. |