гуд работа. Курс лекций теория вычислительных процессов
 Скачать 1.54 Mb.
|
|
Информационные связи и сечения: Превратим принцип Б в систематическое правило “не надо торопиться вводить для результата новое обозначение, а посмотреть, нет ли в данный момент освободившейся величины…” - Это означает, что мы, решая задачу, экономии памяти, должны просмотреть операторы про- граммы в порядке их выполнения. - Тогда (в случае линейной программы) выше очередного рассматриваемого нами оператора будут операторы уже выполнившиеся, а ниже будут команды еще не выполнившиеся. Мы не торопимся ввести новую величину для результата очередного оператора S, а смотрим на ве- личины, обозначающие результаты операторов, стоящих выше. - Что значит, что величина V, которая есть результат оператора R, еще не освободилась? ++ Это значит, что ниже оператора S есть еще один оператор T, имеющий V своим аргумен- том. Рассмотрим разнообразие вариантов выборки и использования велечины V по отношению к оператору S. R: V := … R: V := … R: V:= … R: V:=… S: X :=… T’: Z := F’(V) T’: Z:=F’(V) T’: Z:= F’(V) T: Z := F(V) S: X:= … S: X:=… S: X:=… T: Z:=F(V) R’: V:=… T: Z := F(V) Случай а) Случай б) Случай в) - величины V «занята” по отношению к оператору S, если S находится между выработкой V (оператор R) и использованием V (оператор T) при этом между S и T нет оператора, вырабатывающего V. R: V := … S: X := … T: Z := F(V) Начало вещ x, y, x2, x4, x8, x16, x32 Ввод (x) x2 := x * x; x4 := x2 * x2; x8 := x4 * x4; x16 := x8 * x8; x32 := x16 * x16; y := x * x2; y := y * x8; y := y * x16; y := y * x32; Вывод (y) Конец Обозначим все пути от результатов к аргументам, как мы указали выше и получим достаточно большое количество связей. Назовем их информационными связями между аргументами и результатами операторов. Все эти связи будут ориентированы “вдоль” по направлению выполнения программы. Анализ этих связей дает нам полное представление о том, как надо распределить память в программе: - подчеркнем каждый оператор горизонтальной линией, обозначающей момент выполнения этого оператора. Эта линия – сечение программы. - тогда число информационных связей, пересекаемых сечением, показывает, сколько в настоя- щий момент “занято”, т.е. используется для хранения результатов, которые выработаны раньше, но потребуются позднее, а символы величины, сопоставленных концевым тыкам этих “маршрутов” указывают, какие конкретно величины используются. 8 9 2. Верификация программ Основные понятия и теоремы Вопрос о правильности написанной программы является одним из самых насущных в програм- мировании. Обычная практика проверки программ состоит в составлении тестов и проверке правильно- сти работы программы на предъявленных тестах. Разумеется, это никогда не дает 100-процентной га- рантии правильности программы, однако, хорошо подобранная система тестов может быть очень убе- дительной. Другой подход состоит в том, чтобы рассматривать программу как математический объект и пы- таться доказать ее правильность методами математического анализа ее текста. В случае если такой ана- лиз возможен, правильность программы будет доказана абсолютно. Более того, если удастся разрабо- тать процедуру доказательства таким образом, что процесс доказательства можно проводить автомати- чески, то проверка правильности программы может свестись к запуску процедуры этой проверки, реа- лизованной в виде компьютерной программы. К сожалению, несмотря на то, что на этом пути получен ряд существенных результатов, полно- стью автоматизировать процедуру доказательства правильности программы не удается. Тем не менее, задачу имеет смысл рассматривать хотя бы для того, чтобы иметь возможность смотреть на программу с точки зрения математического анализа ее текста. Для этого надо в первую очередь разработать поня- тие спецификации программы и понятие соответствия программы своей спецификации, то есть надо понимать, что именно мы вкладываем в понятие правильной программы. Будем рассматривать простой язык программирования, напоминающий по синтаксису Паскаль, но имеющий ряд серьезных ограничений. Ограничения эти не принципиальны для существа рассматри- ваемого вопроса, но позволяют обойтись минимумом технических средств для доказательства правиль- ности программ. Прежде всего, мы будем рассматривать только работу с целыми значениями, кроме того, мы существенно ограничим набор используемых операторов, исключив из него в первую очередь плохо формализуемый оператор перехода goto. Кроме того, в данном разделе мы не будем рассматри- вать вопросы формализации определения и вызова процедур и функций, и не будем рассматривать сложные структуры данных, даже обычные массивы и записи. Поскольку все переменные в нашем языке имеют тип integer, то нет необходимости в описании этих переменных. Будем считать, что переменная описана просто фактом своего появления в програм- ме. Далее, будем считать, что над целыми значениями определены обычные арифметические операции и встроенные арифметические и логические функции, так что мы будем без дополнительных пояснений писать в программе выражения такие, как (x + 1) * (x – y) и другие, подобные этим. Кроме арифметических выражений, будем использовать также логические выражения (но не логические пере- менные) в контексте условных операторов и операторов цикла. Итак, следующие операторы являются операторами, с помощью которых строятся программы на нашем языке программирования. • Пустой оператор skip, который ничего не делает. • Оператор прерывания abort, действие которого заключается в аварийном прерывании рабо- ты программы с неопределенным результатом. • Оператор присваивания x := E, где x – переменная, E – арифметическое выражение. • Последовательное выполнение операторов begin S ; S end 1 2 , где S 1 и S 2 – произволь- ные операторы. Если не возникает двусмысленности, операторные скобки begin и end бу- дем опускать, так что, например, последовательное выполнение нескольких операторов мож- но будет записать как S ; S ;…; S 1 2 n • Условный оператор if B then S else S 1 2 , где B – логическое выражение, а S 1 и S 2 – операторы, с обычной семантикой условного оператора. Как обычно, будем использовать также и краткую форму условного оператора if B then S 1 , считая ее сокращением пол- ной формы if B then S else skip 1 10 Для заданной программы и ее пред- и постусловий можно поставить несколько различных задач. Во-первых, если задана некоторая спецификация P { S } Q, то можно задаться целью проверить ее истинность. Во-вторых, если задана программа S и предусловие P, то можно попытаться найти какое- либо постусловие Q такое, чтобы спецификация P { S } Q была истинной. Сразу же ясно, что искать следует наиболее сильное постусловие, так как более слабые постусловия будут удовлетворять • Оператор цикла while B do S, где B – условное выражение, а S – оператор тела цикла, с обычной семантикой оператора цикла. Как всегда, тело цикла может не исполниться ни разу, если при первом же вычислении выражение B оказалось ложным. Будем говорить, что имеется некоторое состояние переменных программы, если все переменные программы имеют некоторые значения. Будем считать, что программа начинает свою работу в некото- ром состоянии и может закончить свою работу также в некотором состоянии или результат работы мо- жет оказаться неопределенным, например, если программа «зациклилась», выполнила оператор преры- вания abort или попыталась вычислить некорректное значение (например, разделить некоторое число на ноль). Во время работы программа может неоднократно менять состояние переменных, но нас, в ос- новном, будут интересовать только начальное и конечное состояния. Таким образом, программу можно рассматривать как функцию, которая преобразует некоторое начальное состояние переменных в конеч- ное состояние. Заметим, что эта функция может быть неопределенной на некоторых состояниях (если программа, начав свою работу в некотором состоянии, не в состоянии нормально завершить свою рабо- ту), и, кроме того, если поведение программы не строго детерминировано (например, ее поведение мо- жет зависеть от текущего времени выполнения, датчика случайных чисел и т.п.), то она может, начав работу в некотором состоянии, закончить ее в различных состояниях, то есть функция преобразования состояний, определенная этой программой, вообще говоря, не является однозначной. Вместо того чтобы говорить об отдельных состояниях, мы будем говорить о множествах со- стояний. Описывать эти множества мы будем с помощью предикатов, аргументами которых будут пе- ременные программы. Так, например, предикат P(x, y) = {x < y} описывает множество состояний пере- менных программы, в которых значение переменной x меньше значения переменной y. Если в програм- ме используются три переменные x, y и z, то состояние {x=3, y=4, z=0} входит в множество P, а состоя- ние {x=5, y=4, z=2} в него не входит. Разумеется, каждый предикат определяет некоторое множество состояний и обратно, произвольное множество состояний может быть определено подходящим преди- катом (заметим, что, поскольку программы могут работать лишь с конечным числом целых значений, то и различных состояний всего лишь конечное число). Рассмотрим теперь следующую тройку объектов: предикат P, называемый предусловием, про- грамму S и предикат Q, называемый постусловием. Будем говорить, что программа удовлетворяет спе- цификации P { S } Q, если программа S такова, что если она начинает свою работу в некотором состоя- нии, принадлежащем множеству состояний P, то она непременно закончит работу, причем заключи- тельное состояние будет принадлежать множеству состояний Q. Таким образом, спецификация P { S } Q является некоторым высказыванием о программе, которое может быть истинным или ложным в зависимости от того, какие пред- и постусловия используются в этой спецификации. Заметим, что если множество состояний, описываемое предикатом P 1 , является подмножеством множества состояний, описываемых предикатом P 2 , то предикат P 2 является логическим следствием предиката P 1 и наоборот. Отсюда, в частности следует, что если P { S } Q 1 и Q 1 ⇒ Q 2 , то P { S } Q 2 , а также если P 2 { S } Q и P 1 ⇒ P 2 , то P 1 { S } Q. Другими словами, если верна некоторая спецификация программы, то верна также и спецификация с более сильным предусловием и спецификация с более слабым постусловием. В этой формулировке используется понятие более сильного (более слабого) пре- диката. Говорят, что предикат P сильнее, чем Q, если Q является логическим следствием P. Соответст- венно, P слабее, чем Q, если Q сильнее, чем P. Отношение «сильнее» на множестве предикатов является частичным нестрогим порядком, так же, как и соответствующее ему отношение включения множеств состояний. Пустому множеству состояний соответствует тождественно ложный предикат, обозначаемый F. Это самый сильный из всех возможных предикатов, поскольку F ⇒ P верно для любого P. Аналогично, универсальному множеству всех состояний соответствует тождественно истинный предикат, обозна- чаемый T. Это, напротив, самый слабый из возможных предикатов, поскольку является логическим следствием любого другого предиката: P ⇒ T для любого P. 11 наиболее сильное постусловие, так как более слабые постусловия будут удовлетворять спецификации автоматически. В-третьих, если задана программа S и постусловие Q, то можно попытаться найти (сла- бейшее) предусловие P такое, что спецификация P { S } Q будет истинной. В каком-то смысле послед- няя задача является самой естественной, так как нам всегда известна цель программы – то множество состояний, в которых может оказаться правильно работающая программа в конце работы, и мы можем попытаться определить, какие условия надо наложить на начальное состояние переменных программы для того, чтобы программа корректно завершилась. Итак, основной задачей логического анализа (вери- фикации) программы является задача нахождения (слабейшего) предусловия для заданного постусло- вия. Будем говорить, что если задана программа S и постусловие Q, то слабейшее предусловие для этой программы и этого постусловия может быть получено с помощью специальной функции – преоб- разователя предикатов wp (weakest precondition), которая и должна выдавать требуемый результат (P = wp(S, Q)). Можно построить формальную теорию, в которой семантика операторов простого языка программирования задается с помощью аксиом, выражающих результат применения преобразователя предикатов wp к простым операторам, а правила вывода позволяют выводить заключения о слабейшем предусловии для более сложных постусловий и более сложных программ через слабейшие предусловия для более простых постусловий и более простых программ. Разумеется, такая формальная теория долж- на быть построена «разумно», то есть ее аксиомы и правила вывода должны быть такими, чтобы они позволяли получать практически значимые результаты. Будем обосновывать каждую аксиому и каждое правило вывода, исходя из понимания того, как должно меняться состояние переменных программы. Сначала несколько простых аксиом. 1. wp(S, F) ⇔ F для любого оператора S. Эта аксиома носит названия закона «исключенного чуда», поскольку и в самом деле не существует никакого состояния, начавшись в котором программа мо- жет гарантированно завершить свою работу в «никаком» состоянии. 2. wp(skip, Q) ⇔ Q для любого предиката Q. Эта аксиома определяет семантику пустого оператора. Аксиома «разумна», поскольку пустой оператор и в самом деле не меняет состояния переменных, а значит, в каком бы состоянии ни начал работу пустой оператор, он закончит работу в том же самом состоянии. 3. wp(abort, Q) ⇔ F для любого предиката Q. Эта аксиома определяет семантику оператора прерыва- ния. Действительно, не существует такого состояния, начав работу в котором оператор прерывания смог бы завершить работу в некотором состоянии, поэтому данная аксиома также «разумна». 4. wp(S, Q 1 ∧ Q 2 ) ⇔ wp(S, Q 1 ) ∧ wp(S, Q 2 ). Данная аксиома позволяет получать слабейшее предусловие для конъюнкции постусловий, если известны слабейшие предусловия для отдельных членов этой конъюнкции. Обосновать эту аксиому можно, исходя из смысла преобразователя предикатов wp. Действительно, пусть некоторое состояние s ∈ wp(S, Q 1 ∧ Q 2 ). Это означает, что программа S, начав работу в состоянии s, закончит работу в состоянии s 1 , удовлетворяющем условию Q 1 ∧ Q 2 . Но тогда состояние s 1 удовлетворяет условиям Q 1 и Q 2 по отдельности, то есть одновременно s ∈ wp(S, Q 1 ) и s ∈ wp(S, Q 2 ). Тогда s ∈ wp(S, Q 1 ) ∧ wp(S, Q 2 ). Наоборот, если s ∈ wp(S, Q 1 ) ∧ wp(S, Q 2 ), то аналогич- ными рассуждениями можно показать, что тогда также s ∈ wp(S, Q 1 ∧ Q 2 ). В совокупности оба рас- суждения и обосновывают корректность аксиомы. 5. wp(S, Q 1 ) ∨ wp(S, Q 2 ) ⇒ wp(S, Q 1 ∨ Q 2 ). Заметим, что в данной аксиоме предикаты в левой и правой частях аксиомы не обязаны быть эквивалентными, но правая часть является логическим следствием левой. Аксиому можно обосновать рассуждениями, аналогичными тем, которые проводились для предыдущей аксиомы. Заметим, что если программа S имеет детерминированное поведение, то есть, начав работу в некотором начальном состоянии, всегда заканчивает работу в одном и том же конеч- ном состоянии (или всегда не может закончить работу), то в аксиоме для таких программ можно вместо знака логического следствия ⇒ поставить знак логической эквивалентности ⇔. Однако если программа недетерминированная, то эквивалентности может и не быть. Простым примером такой недетерминированной программы может быть программа «бросания монеты» x := random(2), присваивающая переменной x случайное значение 0 или 1. Если в качестве постусловия Q взять предикат |