Теория вычислительных процессов

Доказательство.

Из определения DO следует:

Если H₀(T)= NOT BB AND T, k=0

H_k(T)=wp(IF, H_k-1(T)), k>0, > wp(DO,T)=($ k: k і 0: H_k(T))

H₀(P AND NOT BB)=P AND NOT BB;

H_k(P AND NOT BB)=wp(IF, H_k-1(P AND NOT BB), > wp(DO, P AND NOT BB)=($ k і 0: H_k(P AND NOT BB))

С помощью метода математической индукции можно доказать, что из условия (2.3) следует

(P AND H_k(T)) => H_k(P AND NOT BB), k і 0

Тогда имеем

P AND wp(DO, T) = ($k: k і 0: P and H_k(T) ) => ($k: k і 0: H_k(P AND NOT BB) ) = wp(DO, P AND NOT BB)

Следовательно, (P AND wp(DO, T)) => wp(DO, P AND NOT BB).

Чтобы использовать аксиоматическую семантику с данным языком программирования для доказательства правильности программ или для описания формальной семантики, для каждого вида операторов языка должны быть определены аксиомы или правила логического вывода. С ними мы познакомимся в п. 2.3 «Верификация программ».

В аксиоматической семантике система (2.1) интерпретируется как набор аксиом в рамках некоторой формальной логической системы, в которой есть правила вывода и/или интерпретации определяемых объектов.

Для интерпретации системы функций (2.1) вводится понятие аксиоматического описания <S, A> - логически связанной пары понятий: S - сигнатура используемых в системе символов функций f1, f2, ..., fm и символов констант (нульместных функциональных символов) c1, c2, ..., cI, а A - набор аксиом, представленный системой. Предполагается, что каждая переменная xi, i=1, ..., k, и каждая константа ci, i=1, ..., l, используемая в A, принадлежит к какому-либо из типов данных t1, t2, ..., tr, а каждый символ fj, j=1, ..., m, представляет функцию, типа: ti1? ti2 ... ? tik ti0. Такое аксиоматическое описание получит конкретную интерпретацию, если будут заданы конкретные типы данных ti = ti', i=1, ..., r, и конкретные значения констант ci = ci', i = 1, ..., l.

К. Хоaр построил аксиоматическое определение набора типов данных, которые потом Н. Вирт использовал при создании языка Паскаль.

Пример 2.6. Рассмотрим систему равенств:

УДАЛИТЬ(ДОБАВИТЬ(m,d))=m,

ВЕРХ(ДОБАВИТЬ(m,d))=d,

УДАЛИТЬ(ПУСТ)=ПУСТ,

ВЕРХ(ПУСТ)=ДНО,

где УДАЛИТЬ, ДОБАВИТЬ, ВЕРХ - символы функций, а ПУСТ и ДНО - символы констант, образующие сигнатуру этой системы. Пусть D, D1 и М - некоторые типы данных, такие, что m ? M, d ? D, ПУСТ ? M, ДНО ? D1, а функциональные символы представляют функции следующих типов:

УДАЛИТЬ: M ® M,

ДОБАВИТЬ: M, D ® M,

ВЕРХ: M ® D1.

Данная сигнатура вместе с указанной системой равенств, рассматриваемой как набор аксиом, образует аксиоматическое описание абстрактного типа данных, называемого магазином.

Зададим интерпретацию символов ее сигнатуры: D - множество значений, которые являются элементами магазина, M - множество состояний магазина,

M = {d₁,d₂, ... ,d_n: d_i О D, i=1, ..., n, n і 0}, D1=D И {ДНО}, ПУСТ={},

а ДНО - особое значение (зависящее от реализации магазина), не принадлежащее D. Тогда указанный набор аксиом определяют свойства магазина.

При определении семантики полного языка программирования с использованием аксиоматического метода для каждого вида операторов языка должны быть сформулированы аксиома или правило логического вывода. Но определение аксиом и правил логического вывода для некоторых операторов языков программирования - очень сложная задача. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства утверждений о программах» (Э. Дейкстра).

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

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

2.1.3 Денотационная семантика

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

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

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

<двоичное_число> > 0

| 1

| <двоичное_число> 0

| <двоичное_число> 1

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

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

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

Мb('0') = 0, Мb('1')=1

Мb(<двоичное_число> '0') = 2 * Мb(<двоичное_число>)

Мb(<двоичное_число> `1') = + 2 * Мb(<двоичное_число>) + 1

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

Пример 2.7. Описание значения десятичных синтаксических литеральных констант.

<десятичное_число> > 0|1|2|3|4|5|6|7|8|9

| <десятичное_число> (0|1|2|3|4|5|6|7|8|9)

Денотационные отображения для этих синтаксических правил имеют следующий вид:

Md(`0') = 0, Md('1') = 1, ,..., Md('9') = 9

Мd(<десятичное_число> '0') = 10 * Мd(<двоичное_число>)

Мd(<десятичное_число> `1') = 10 * Мd(<десятичное_число>) + 1

…

Мd(<десятичное_число> '9') = 10 * Мd(<десятичное_число>) + 9

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

{<i1, v1>, <i2, v2>, …, <in, vn>}.

Каждый параметр i является именем переменной, а соответствующие параметры v являются текущими значениями данных переменных. Любой из параметров v может иметь специальное значение undef, указывающее, что связанная с ним величина в данный момент не определена.

Пусть VARMAP - функция двух параметров, имени переменной и состояния программы. Значение функции VARMAP(ik, s) равно vk (значение, соответствующее параметру ik в состоянии s).

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

Выражения являются основой большинства языков программирования. Более того, мы имеем дело только с очень простыми выражениями. Единственными операторами являются операторы + и *; выражения могут содержать не более одного оператора; единственными операндами являются скалярные переменные и целочисленные литеральные константы; круглые скобки не используются; значение выражения является целым числом. Ниже следует описание этих выражений в форме БНФ:

<выражение> > <десятичное_число> | <переменная>

| <двоичное_выражение>

<двоичное_выражение> > <выражение_слева> <оператор>

<выражение_справа>

<оператор> > + | *

Единственной рассматриваемой нами ошибкой в выражениях является неопределенное значение переменной. Разумеется, могут появляться и другие ошибки, но большинство из них зависят от машины. Пусть Z - набор целых чисел, a error - ошибочное значение. Тогда множество Z {error} является множеством значений, для которых выражение может быть вычислено.

Ниже приведена функция отображения для данного выражения Е и состояния s. Символ обозначает равенство по определению функции.

Me (<выражение>,s)

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 M_e(E, s) = error

then error

else s' = {< i₁', v₁' >, < i₂', v₂' >,..., < i_n', v_n' >} where

for j = 1, 2, ..., n, v_j' = VARMAP(i_j', s) if i_j <>x;

M_e(E, s) if i_j = x

Отметим, что два сравнения, выполняющиеся в двух последних строках (ij<> x и ij = х), относятся к именам, а не значениям.

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

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

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

2.1.4 Декларативная семантика

Декларативная семантика является существенной характеристикой языков логического программирования, в которых программы состоят из объявлений (деклараций), а не из операторов присваивания и управляющих операторов. Эти объявления в действительности являются операторами, или высказываниями, в символьной логике.

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

Формальное определение семантики становится общепринятой частью определения нового языка. Стандартное описание языка PL/I включает в себя VDL-подобную нотацию, описывающую семантику операторов PL/I, а для языка Ada было разработано определение на основе денотационной семантики. Тем не менее, изучение формальных определений семантики не оказало такого сильного влияния на практическое определение языков, как изучение формальных грамматик -- на определение синтаксиса. Ни один из методов определения семантики не оказался по настоящему полезным ни для пользователя, ни для разработчиков компиляторов языков программирования.

2.2 Языки формальной спецификации

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

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

описать эскизную модель (функциональности, поведения);

доказать, что модель корректна (не противоречива, консистентна);

детализировать (уточнить) модель;

доказать, что детализация проведена корректно;

повторять два предыдущих шага до тех пор, пока не будет получена готовая программа.

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

У специализированных языков несколько другая история. Некоторые из них, например SDL (Specification and Design Language), родились из практики проектирования систем релейного управления, где проект традиционно был больше похож на чертеж, чем на текстовое (языковое) описание. Здесь эволюция заключалась во взаимном сближении графической и текстовой нотации на основе взаимных компромиссов и ограничений. При этом участниками компромисса была некоторая графическая нотация и языки программирования, опыт, накопленный в других языках формальных спецификаций, либо игнорировался, либо заимствовался с большим опозданием.

ЯФС традиционно рассматривались как средство проектирования. Новый взгляд на ЯФС появился когда стала актуальной задача анализа уже существующего программного обеспечения. Существенное продвижение на этом фронте было связано с направлением Объектно-Ориентированного Анализа. Его идеи во многом созвучны с Объектно-Ориентированным Проектированием. Не удивительно, что оба эти направления предлагают близкие изобразительные средства для описания архитектуры и поведения систем. В последнее время наиболее известным средством такого рода является (преимущественно) графический язык UML (Unified Modelling Language). Заметим, что UML и подобные ему языки спецификации, безусловно, являются неплохими средствами проектирования, но обычно непригодны для доказательства правильности, на что делался акцент в классических языках спецификации.

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

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

Исполнимые спецификации, исполнимые модели. Этот подход предполагает разработку прототипов (моделей) систем для демонстрации возможности достижения поставленной цели и проведения экспериментов при частичной реализации функциональности. Примерами таких методологий и языков являются SDL, RSL (RAISE Specification Language).

Алгебраические спецификации предполагают описание свойств композиций операций. Композиции могут быть последовательными, параллельными, с временными ограничениями и без. Преимуществом этого подхода является то, что в идеале можно полностью абстрагироваться от структур данных, которые используются в качестве входных и выходных значений и, возможно, используются для сохранения внутреннего состояния моделей. Основной недостаток - это нетрадиционность приемов спецификации, что затрудняет их внедрение в промышленных разработках. В качестве примера языка алгебраических спецификаций можно назвать ASN1 (Abstract Syntax Notation One), стандарт которого входит в группу стандартов, описывающих SDL, RSL.

Сценарные спецификации описывают не непосредственно целевую систему, а способы ее использования или взаимодействия с ней. Оказывается, что такие косвенные описания, с одной стороны, позволяют судить о некоторых свойствах системы (тем самым, они, конечно, являются спецификациями), и, с другой стороны, такие спецификации могут служить хорошим руководством по использованию системы, что не всегда можно сказать о других видах спецификаций. Наибольшее распространение получили работы OMG группы и продукты компании Rational Corporation.

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

2.3 Верификация программ

2.3.1 Методы доказательства правильности программ

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

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

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

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

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

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

Метод установления правильности программ при помощи строгих средств известен как верификация программ.

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

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

спецификацию ввода-вывода (описание данных, не зависящих от процесса обработки);

свойства отношений между элементами векторов состояний в выбранных точках программы;

спецификации и свойства структурных подкомпонентов программы;

спецификацию структур данных, зависящих от процесса обработки.

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

Суть этого метода состоит в следующем:

1) формулируются входное и выходное утверждения: входное утверждение описывает все необходимые входные условия для программы (или программного фрагмента), выходное утверждение описывает ожидаемый результат;

2) предполагая истинным входное утверждение, строится промежуточное утверждение, которое выводится на основании семантики операторов, расположенных между входом и выходом (входным и выходным утверждениями); такое утверждение называется выведенным утверждением;

3) формулируется теорема (условия верификации):

из выведенного утверждения следует выходное утверждение;

4) доказывается теорема; доказательство свидетельствует о правильности программы (программного фрагмента).

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

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

из входного утверждения следует выведенное утверждение.

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

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

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

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

1) Построить структуру программы.

2) Выписать входное и выходное утверждения.

3) Сформулировать для всех циклов индуктивные утверждения.

4) Составить список выделенных путей.

5) Построить условия верификации.

6) Доказать условие верификации.

7) Доказать, что выполнение программы закончится.

Этот метод сравним с обычным процессом чтения текста программы (метод сквозного контроля). Различие заключается в степени формализации.

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

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

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

Отметим трудности, связанные с методом индуктивных утверждений. Трудно построить «множество основных аксиом, достаточно ограниченное для того, чтобы избежать противоречий, но достаточно богатое для того, чтобы служить отправной точкой для доказательства утверждений о программах» (Э. Дейкстра). Вторая трудность - семантическая, заключающаяся в формировании самих утверждений, подлежащих доказательству. Если задача, для которой пишется программа, не имеет строгого математического описания, то для нее сложнее сформулировать условия верификации.

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

Метод, который сформулировали К. Хоар и Э. Дейкстра основан на формальном выводе программ из математической постановки задачи.

2.3.2 Использование утверждений в программах

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

Исчисление - это метод или процесс рассуждений посредством вычислений над символами. В исчислении предикатов утверждения являются логическими переменными или выражениями, имеющими значение T - истина или F - ложь. Наша цель - при написании программы некоторым способом доказать истинность утверждения (2.2) - триады Хоара {Q} S {R}. Для этого нужно уметь записывать его в исчислении предикатов и формально доказывать его истинность.

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

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

s = sqrt(n),

где n, s О Nat. Определим постусловие в виде:

R: s*s Ј n < (s+1)*(s+1)..

Пример 2.9. Даны целочисленные n > 0 и массив a[1,...,n]. Отсортировать массив, т.е. установить

R: (" i: 1 Ј i < n: a[i] Ј a[i+1]).

Пример 2.10. Определить x как максимальное значение массива a[1,...,n]. Определим постусловие:

R: {x = max({y | y Н a})}.

Для построения программы следует определить математическое понятие max. Тогда

R: {($ i: 1 Ј i Ј n: x = a[i]) AND (" i: 1 Ј i Ј n: a[i] = x)}.

Пример 2.11. Пусть имеем программу S обмена значениями двух целых переменных a и b. Сформулируем входное и выходное утверждения программы и представим программу S в виде предиката:

{ a = A AND b = B } S { a = B AND b = A }, (2.4)

где A, B - конкретные значения переменных a, b.

Программа вместе с утверждениями между каждой парой соседних операторов называется наброском доказательства. Последовательно, для каждого оператора программы формулируя предикат (2.4), можно доказать, что программа удовлетворяет своим спецификациям. Представим набросок доказательства для программы S:

{ a = A AND b = B }

r := a; { r = a AND a = A AND b = B };

a := b; { r = a AND a = B AND b = B };

b := r; { a = B AND b = A }.

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

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

2.3.3 Правила верификации К. Хоара

Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.

A1. Аксиома присваивания: { Ro } x := Е { R }

Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, Ro = R(x) при x = E. Для Ro вводится обозначение: Ro = RxЕ (у Вирта) или Rx>Е (у Дейкстры), что означает, что x заменяется на Е.

Аксиома присваивания будет иметь вид:{RxЕ} x := Е {R}.

Сформулируем два очевидных правила монотонности.

A2. Если известно: { Q } S { P } и { P } => { R }, то { Q } S { R }

A3. Если известно: { Q } S { P } и { R } => { Q }, то { R } S { P }

Пусть S - это последовательность из двух операторов S1; S2 (составной оператор).

A4. Если известно:{ Q } S1 { P1 } и { P1 } S2 { R }, то { Q } S { R }.

Это правило можно сформулировать для последовательности, состоящей из n операторов.

Сформулируем правило для условного оператора (краткая форма).

A5. Если известно:

{ Q AND B } S1 { R } и { Q NOT B } => { R },то { Q } if B then S1 { R }.

Правило A5 соответствует интерпретации условного оператора в языке программирования.

Сформулируем правило для альтернативного оператора (полная форма условного оператора).

A6. Если известно: { Q AND B } S1 { R } и { Q NOT B } S2 { R },то { Q } if B then S1 else S2 { R }.

Сформулируем правила для операторов цикла.

Предусловия и постусловия цикла until удовлетворяют правилу:

A7. Если известно: { Q AND NOT B } S1 { Q }, то { Q } repeat S1 until B { Q AND NOT B }

Правило отражает инвариантность цикла. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале.

Предусловия и постусловия цикла while удовлетворяют правилу:

A8. Если известно: { Q AND B } S1 { Q } , то { Q } while B do S1 { Q AND NOT B }

Правила A1 - A8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла и для анализа результатов выполнения программы.

Пример 2.12. Пусть надо определить частное q и остаток r от деления x на y.

Входные данные x, y и выходные данные q, r Nat, причем y > 0.

Задать(x,y); /* x,y получают конкретные значения X,Y */

r := x; q := 0;

while y Ј r do

begin

r := r - y; q := q + 1

end;

выдать(q,r);

Сформулируем постусловие

R: (r < y) AND (x = y*q + r)

Нужно доказать, что

{y > 0 AND x/y} S {(r < y) AND (x = y*q + r )}.

Доказательство.

Очевидно, что

Q => x = x + y * 0.

Применим аксиому A1 к оператору r := x, тогда получим

{ x = x + y * 0 } r := x { x = r + y * 0 }

Аналогично, применяя A1 к оператору q := 0, получим:

{ x = r + y * 0 } q := 0 { x = r + y*q }

Применяя правило A3 к результатам пунктов 1 и 2, получим

{ Q } r := x { x = r + y * 0 }

Применяя правило A4 к результатам пунктов 4 и 3, получим

{ Q } r := x; q := 0 { x = r + y*q }

Выполним равносильное преобразование

x = r + y * q AND y ? r => x = (r - y) + y*(q + 1)

Применяя правило A1 к оператору r:= r - y, получим

{x = (r - y) + y*( q + 1)} r:= r - y {x = r+ y*(q+1)}

Для оператора q := q + 1 аналогично получим

{ x = r + y*(q + 1) } q := q + 1 { x = r + y*q }

Применяя правило A4 к результатам пунктов 7 и 8, получим

{ x = (r - y) + y*( q + 1) } r := r - y; q := q + 1 { x = r + y*q }

Применяя правило A2 к результатам пунктов 6 и 9, получим

{ x = r + y*q AND y Ј r } r := r - y; q := q + 1 { x = r + y*q }

Применяя правило A8 к результату пункта 10, получим

{x = r + y*q } while y Ј r do begin r := r - y; q := q + 1 end { NOT (y <= r) AND (x = r + y*q) }

Утверждение x = r + y*q является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.

Применяя правило A4 к результатам пунктов 5 и 11, получаем то, что требовалось доказать,

{ Q } S { NOT (y Ј r) AND (x = r + y*q) }

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

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

1) y Ј r;

2) r, q О Nat.

Но значение r на каждом шаге цикла уменьшается на положительную величину: r := r - y (y > 0). Значит, последовательность значений r и q является конечной, т.е. найдется такое значение r, для которого не будет выполняться условие y Ј r и циклический процесс завершится.

3. Теоретические модели вычислительных процессов

3.1 Взаимодействующие последовательные процессы

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

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

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

В-третьих, он является надежной основой для избежания таких ошибок, как расходимость, тупики, зацикливание.

3.1.1 Определения

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

«Задача - основная единица, подчиняющаяся управляющей программе в мультипрограммном режиме»; «Процесс - это программа, выполняемая псевдопроцессором»; «Процесс - это то, что происходит при выполнении программы на ЭВМ».

Хорнинг и Ренделл (1973) построили формальное определение понятие процесса.

Основные термины модели:

набор переменных состояния;

состояние;

пространство состояний;

действия;

работа;

функция действия;

процесс;

начальное состояние.

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

В случае простого автомата, торгующего шоколадками, существуют два вида событий;

мон - опускание монеты в щель автомата,

шок - появление шоколадки из выдающего устройства.

Заметим, что имя каждого события обозначает целый класс событий; отдельные вхождения события внутри одного класса разделены во времени. Множество имен событий, выбранных для конкретного описания объекта, называется его алфавитом.

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

Введем следующие соглашения:

Имена событий будем обозначать словами, составленными из строчных букв, например, шок, а также буквами а, b, с...

Имена процессов будем обозначать словами, составленными из прописных букв, например, ТАП -- простой торговый автомат, а буквами Р, Q, R будем обозначать произвольные процессы.

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

Буквы А, В, С используются для обозначения множества событий.

Буквы X, У используются для переменных, обозначающих процессы.

Алфавит процесса Р обозначается ?Р, например, ?ТАП = {мон, шок}.

Процесс с алфавитом V, такой, что в нем не происходит ни одно событие из V, назовем СТОПA. этот процесс описывает поведение сломанного объекта. Далее определим систему обозначений, которая также предназначена для описания поведения объектов.

3.1.1.1 Префиксы

Пусть х -- событие, а Р -- процесс. Тогда (х ® Р) (читается как «Р за х») описывает объект, который вначале участвует в событии х, а затем ведет себя в точности как Р, где

a(х ® Р) = aР, x О aР.

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

(мон ® (шок ® (мон ® (шок ® СТОП_aТАП)))).

В дальнейшем скобки будут опускаться в случае линейной последовательности событий. Условимся, что операция > ассоциативна справа.

3.1.1.2 Рекурсия

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

Рассмотрим простой долговечный объект -- часы, функционирование которых состоит в том, чтобы тикать.

aЧАСЫ = {тик}.

Теперь рассмотрим объект, который вначале издает единственный «тик», а затем ведет себя в точности как ЧАСЫ

(тик®ЧАСЫ).

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

ЧАСЫ = (тик®ЧАСЫ).

Это уравнение можно развертывать простой заменой в правой части уравнения члена ЧАСЫ на равное ему выражение (тик?ЧАСЫ) столько раз, сколько нужно, при этом возможность для дальнейшего развертывания сохраняется. Мы эффективно описали потенциально бесконечное поведение объекта ЧАСЫ, как

тик ® тик ® тик ®…

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

Утверждение 3.1. Если F(Х) -- предваренное выражение, содержащее имя процесса X, а V -- алфавит X, то уравнение Х = F(Х) имеет единственное решение в алфавите V.

Иногда обозначают это решение выражением

mХ: V.F(Х).

Пример 3.2. Простой торговый автомат, полностью удовлетворяющий спрос на шоколадки:

ТАП = (мон ® (шок ® ТАП)).

Решение этого уравнения может быть записано в виде Т

АЛ = Х: {мон, шок}.(мон ® (шок ® X)).

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

3.1.1.3 Выбор

Используя префиксы и рекурсию, можно описывать объекты, обладающие только одной возможной линией поведения. Однако поведение многих объектов зависит от окружающей их обстановки. Например, торговый автомат может иметь различные щели для 1- и 2-пенсовых монет; выбор одного из двух событий в этом случае предоставлен покупателю.

Если х и y -- различные события, то

(х ® P | у ® Q)

описывает объект, который сначала участвует в одном из событий x, у, где a(х ® P | у ® Q) = aP, x, y О aР и aР = aQ.. Последующее же поведение объекта описывается процессом Р, если первым произошло событие х, или Q, если первым произошло событие y.

Пример 3.3. Процесс копирования состоит из следующих событий:

вв.0 -- считывание нуля из входного канала,

вв.1 -- считывание единицы из входного канала,

выв.0 -- запись нуля в выходной канал,

выв.1 -- запись единицы в выходной канал.

Поведение процесса состоит из повторяющихся пар событий. На каждом такте он считывает, а затем записывает один бит.

КОПИБИТ=mХ: (вв.0 ® выв.0 ® X | вв.1 ® выв.1 ® X).

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

(х: В ® Р(х))

определяет процесс, который сначала предлагает на выбор любое событие у из В, а затем ведет себя как Р(у).

3.1.1.4 Взаимная рекурсия

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

Пример 3.4. Автомат с газированной водой имеет рукоятку с двумя возможными положениями -- ЛИМОН и АПЕЛЬСИН. Действия по установке рукоятки в соответствующее положение назовем устлимон и устапельсин, а действия автомата по наливанию напитка -- лимон и апельсин. Вначале рукоятка занимает некоторое нейтральное положение, к которому затем уже не возвращается. Ниже приводятся уравнения, определяющие алфавит и поведение трех процессов:

aАГАЗ = aG = aW = {устлимон, устапельсин, мон, лимон, апельсин}.

АГАЗ = (устлимон ® G | устапельсин ® W),

G = (мон ® лимон ® G | устапельсин ® W),

W = (мон ® апельсин ® W | устлимон ® G).

3.1.2 Законы

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

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

L1. (х: А ® Р(х)) = (у: В ® Q(у)) є (А = В AND "х О А.Р(х) = Q(х))

Этот закон имеет ряд следствий:

L1A. СТОП № (a ® P).

Доказательство: ЛЧасть = (х: {} ® P) № (х: {a} ® Р) = ПРЧасть, так как {} № {a}.

L1B. (с ® Р) ? ( d® Q), если с ? d.

Доказательство: Так как, {с} ? {d}.

L1C. (с ® Р | d® Q) = (d ® Q | с ® Р).

L1D. (с ® Р) = (с ® Q) є Р = Q.

Доказательство: Так как, {с} = {с}.

С помощью этих законов можно доказывать простые теоремы.

Пример 3.5. (мон ® шок ® мон ® шок ® СТОП) ® (мон v СТОП).

Доказательство: Следует из L1B и L1A.

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

L2. Если F(X) -- предваренное выражение, то (Y = F(Y)) ® (Y = ®X.F(X)).

Как прямое следствие получаем, что mX.F(X) является решением соответствующего уравнения

L2A. mX.F(X) = F(mX.F(X)).

Пример 3.6. Пусть ТА1 = (мон ® ТА2), а ТА2 = (шок ® ТА1). Требуется доказать, что ТА1 = ТАП.

Доказательство: ТА1 = (мон ® ТА2) = по определению ТА1

= (мон ® (шок ® ТА1)) по определению ТА2

Таким образом, ТА1 является решением того же рекурсивного уравнения, что и ТАП. Так как это уравнение предварённое, оно имеет единственное решение. Значит, ТА1 = ТАП.

3.1.3 Реализация процессов

Любой процесс Р, записанный с помощью введенных обозначений, можно представить в виде

(х: В ® F(х)).

где F -- функция, ставящая в соответствие множеству символов множество процессов. Множество В может быть пустым (в случае P = СТОП), может содержать только один элемент (в случае префикса) или -- более одного элемента (в случае выбора).