гуд работа. Курс лекций теория вычислительных процессов
 Скачать 1.54 Mb.
|
|
Q 1 ∨ Q 2 , где Q 1 ⇔ { x = 0 } и Q 2 ⇔ { x = 1 }, то, очевидно, wp(S, Q) ⇔ T, поскольку после выполнения программы S переменная x непременно окажется равной либо 0, либо 1. В то же время нет никакой гарантии, что эта переменная непременно окажется равной нулю, так что wp(S, Q 1 ) ⇔ F 12 и, аналогично, wp(S, Q 2 ) ⇔ F. Таким образом, видно, что для такой программы и такого постусловия левая и правая части аксиомы не эквивалентны, но аксиома все же верна, поскольку F ⇒ T. 6. wp(begin S 1 ; S 2 end, Q) ⇔ wp(S 1 , wp(S 2 , Q)). Аксиома для последовательности из двух операторов очевидна. Чтобы завершить систему аксиом, надо еще задать аксиомы для оставшихся операторов – опера- тора присваивания, условного оператора и оператора цикла. Эти аксиомы, однако, не такие простые и требуют дополнительных пояснений. Оператор присваивания меняет состояние переменных программы таким образом, что ровно од- на переменная меняет свое значение, причем новое значение переменной вычисляется в правой части оператора присваивания. Оператор присваивания x := E всегда заканчивается нормально за исключе- нием случаев, когда правая часть не может быть вычислена. Обозначим через D(E) «область определе- ния E» – предикат, задающий множество состояний переменных, в каждом из которых правая часть присваивания вычисляется нормально. Тогда естественной представляется следующая аксиома опера- тора присваивания: wp(x := E, Q) ⇔ D(E) ∧ Q{x/E}, где через Q{x/E} обозначен результат подста- новки в предикат Q выражения E вместо всех вхождений переменной x. Приведем простые примеры, показывающие, что аксиома оператора присваивания действитель- но позволяет находить слабейшие предусловия для программ, содержащих оператор присваивания. В первом примере рассмотрим простой оператор x := x + 1 и постусловие x > 0. Согласно аксиоме для оператора присваивания слабейшим предусловием для заданных оператора и постусловия будет wp(x := x + 1, x > 0) = D(x + 1) ∧ x + 1> 0. Область определения выражения x + 1 есть условие x < maxint, где maxint – максимальное целое значение. Таким образом, искомое слабей- шее предусловие может быть задано предикатом -1 < x < maxint. Во втором примере рассмотрим последовательность операторов присваивания x := y – x; y := y – x; x := x + y и постусловие x = A ∧ y = B, где A и B – некоторые целые константы. Полагая для простоты выражения всегда вычислимыми (то есть, игнорируя «область определения» правых частей операторов присваивания), согласно аксиомам для оператора присваивания и последовательности операторов получим wp(x := y – x; y := y – x; x := x + y, x = A ∧ y = B) ⇔ wp(x := y – x, wp(y := y – x, wp(x := x + y, x = A ∧ y = B))) ⇔ wp(x := y – x, wp(y := y – x, x + y = A ∧ y = B)) ⇔ wp(x := y – x, wp(y := y – x, x = A - B ∧ y = B)) ⇔ wp(x := y – x, x = A - B ∧ y – x = B) ⇔ wp(x := y – x, x = A - B ∧ y = A) ⇔ y – x = A - B ∧ y = A ⇔ x = B ∧ y = A Тем самым доказано, что данная последовательность операторов приводит к тому, что перемен- ные x и y обмениваются значениями. Если все же дополнить рассуждения «областями определения» правых частей всех операторов присваивания, то получим в результате дополнительное условие, со- стоящее в том, что выражение A - B должно быть вычислимо (проверьте это!). Аксиома условного оператора выглядит довольно громоздко, но вполне естественно: wp(if B then S 1 else S 2 , Q) ⇔ (B → wp(S 1 , Q)) ∧ (¬B → wp(S 2 , Q)) Примером применения этой аксиомы может служить доказательство того факта, что программа M: if x < y then z := y else z := x вычисляет максимальное из начальных значений пере- менных x и y. Действительно, если в качестве постусловия взять предикат z = max(x, y), (заметим, что x и y не изменяются в ходе работы программы), то после некоторых преобразований получим: wp(M, z = max(x, y)) ⇔ wp(M, z = x ∧ x ≥ y ∨ z = y ∧ y ≥ x) ⇔ (x < y → wp(z := y, z = x ∧ x ≥ y ∨ z = y ∧ y ≥ x)) ∧ (x ≥ y → wp(z := x, z = x ∧ x ≥ y ∨ z = y ∧ y ≥ x)) ⇔ (x ≥ y ∨ y = x ∧ x ≥ y ∨ y = y ∧ y ≥ x) ∧ (x < y ∨ x = x ∧ x ≥ y ∨ x = y ∧ y ≥ x) ⇔ 13 x ≥ y ∨ x = y ∨ y ≥ x Последний полученный предикат, очевидно, всегда истинен. Значит, слабейшим предусловием для данной программы является тождественно истинный предикат T. Это и означает, что программа достигает нужного результата независимо от начального состояния переменных программы. Для оператора цикла while B do S, к сожалению, невозможно указать формулу, по которой слабейшее предусловие определяется столь же просто, что и для операторов присваивания и условного оператора. Соответствующая аксиома не дает рецепта нахождения слабейшего предусловия, хотя и оп- ределяет его строго и точно. Для этого сначала определяется последовательность предикатов P i , задаю- щие слабейшие предусловия, при которых цикл завершится не более чем за i шагов, и результирующее состояние будет удовлетворять постусловию Q: P 0 = ¬B ∧ Q (цикл завершается за 0 шагов) P i+1 = P 0 ∨ (B ∧ wp(S, P i )) (цикл завершается не более, чем за i+1 шаг) Теперь уже аксиома может быть сформулирована полностью: wp(while B do S, Q) ⇔ ∃i(i ≥ 0 → P i ) или, другими словами, должно найтись такое неотрицательное i, что цикл завершится не более чем за i шагов, причем заключительное состояние будет удовлетворять условию Q. Очевидно, что применить аксиому непосредственно в большинстве случаев невозможно, по- скольку невозможно выписать всю последовательность условий, да еще и сформулировать, когда по крайней мере одно из этих условий будет истинным. Однако в некоторых случаях это все же возможно. Рассмотрим, например, простой цикл while x < 5 do x := x + 1, и постусловие x = 5. Дока- жем, что слабейшим предусловием для этого цикла будет x ≤ 5 . Действительно, очевидно, что P 0 = (x = 5). Докажем (по индукции), что P i = (5-i ≤ x ≤ 5). База индукции только что доказана. Пусть теперь утверждение справедливо для P i . Докажем, что тогда оно справедливо и для P i+1 . Действительно, поскольку P i+1 = P 0 ∨ (B ∧ wp(S, P i )), то по индукционному предположению P i+1 = (x = 5) ∨ (x < 5 ∨ 5-i ≤ x+1 ≤ 5), что и в самом деле (напомним, что мы имеем дело только с целыми числами) эквивалентно выражению 5-(i+1)≤ x ≤ 5. Теперь очевидно, что истинное P i найдется при некотором i тогда и только тогда, когда x ≤ 5. Итак, мы доказали, что wp(while x < 5 do x := x + 1, x = 5) ⇔ x ≤ 5. На практике обычно условия P i так просто определить не удается. Поэтому вместо аксиомы цик- ла используется теорема о цикле, которая позволяет «угадать» предусловие и доказать, что оно и в са- мом деле может служить предусловием в спецификации цикла. Теорема формулируется следующим образом. Теорема (о цикле): если существуют предикат I (называемый в дальнейшем инвариантом цикла) и целочисленная функция f от переменных программы, принимающая только неотрицательные значе- ния (называемая в дальнейшем функцией спуска) такие, что выполнены следующие 4 условия: 1. I ∧ ¬B ⇒ Q 2. I ∧ B ⇒ wp(S, I) 3. f = 0 ⇒ ¬B 4. f = V ∧ B ⇒ wp(S, f < V) (для любой положительной константы V) то I ⇒ wp(while B do S, Q). Другими словами, если удается подобрать инвариант I такой, что выполнены два первых из че- тырех условий теоремы и доказать, что цикл завершается за конечное число шагов (к этому сводятся вторые два условия теоремы), то этот инвариант может служить предусловием для заданных цикла и постусловия. Например, для цикла while x < 5 do x := x + 1 и постусловия x = 5 можно на осно- вании теоремы доказать, что условие x ≤ 5 действительно является предусловием цикла, если рас- сматривать его как инвариант цикла. В самом деле, условие (1) превращается в x ≤ 5 ∧ x ≥ 5 ⇒ x = 5, и, конечно, очевидно; условие (2) превращается в 14 x ≤ 5 ∧ x < 5 ⇒ x + 1 ≤ 5, что, разумеется, также очевидно, а в качестве функции спуска можно взять функцию f(x) = |5 – x|, для которой, очевидно, выполнены оба условия теоремы. Более содержательным примером применения теоремы о цикле может служить доказательство правильности программы быстрого возведения в степень. На этом примере можно также показать, как программа строится одновременно с доказательством ее правильности, то есть инвариант цикла приду- мывается еще до того, как программа написана. Пусть требуется написать программу, которая для заданных значений X и Y>0 вычисляет значе- ние X Y . Постусловие для данной программы можно определить следующим образом: z = X Y , где z – не- которая переменная программы, а X и Y – упомянутые константы. Если x и y – переменные, начальные значения которых равны X и Y соответственно, то перед началом выполнения программы справедливо равенство x y = X Y , и, если положить начальное значение z = 1, то можно предложить в качестве инвари- анта цикла условие z * x y = X Y . Это условие, очевидно, будет выполнено перед началом работы про- граммы, и оно превращается в требуемое постусловие, когда значение переменной y = 0. Для того, что- бы удовлетворить все условия теоремы, надо написать цикл так, чтобы в процессе работы цикла значе- ние y уменьшалось до нуля, при этом условие инварианта должно сохраняться после каждой итерации. Простейшим вариантом такого цикла будет следующий: while y <> 0 do begin y := y – 1; z := z * x end Легко проверить, что для такого цикла все условия теоремы о цикле выполнены. Действительно, условие (1) выполнено, поскольку z * x y = X Y ∧ y = 0 эквивалентно условию z = X Y ∧ y = 0, из которого непосредственно следует требуемое постусловие. Условие (2) также выполнено, поскольку wp(S, I) в данном случае есть z *x * x y-1 = X Y , и, значит, совпадает с инвариантом. Для положительного начального значения y цикл, очевидно, завершается, и мы не будем подбирать функцию спуска ввиду очевидности этого факта (заметим, что, строго говоря, условие неотрицательности y следовало бы добавить в инва- риант цикла, который в этом случае приобретает вид z * x y = X Y ∧ y ≥0). Однако, последовательные умножения на x – это далеко не самый эффективный способ вычис- ления степени. Например, при четном y инвариант цикла сохранится при выполнении другой последо- вательности операторов тела цикла: begin y := y / 2; x := x * x end (легко проверить, что и в этом случае I ⇔ wp(S, I)). Поскольку условие инварианта необходимо сохра- нять при нечетном y так же, как и при четном, то хорошим способом вычисления степени будет сле- дующий цикл: while y <> 0 do if odd(y) then begin y := y – 1; z := z * x end else begin y := y / 2; x := x * x end (здесь логическая функция odd проверяет нечетность аргумента y). Эквивалентность I ⇔ wp(S, I)) для модернизированного тела цикла можно проверить и чисто формальными методами. Задачи 1. Верна ли следующая спецификация программы: x < 5 { x := 2*x } x < 15 Решение: можно рассуждать неформально. Если до начала выполнения программы значение пере- менной x было меньше пяти, то после удваивания это значение будет заведомо меньше десяти, тем более будет справедливо условие x < 15 (полагаем, что удвоение всегда выполнимо). Можно рассу- ждать и более формально. Для этого для заданной программы и постусловии найдем слабейшее пре- дусловие wp(x := 2*x, x < 15) согласно аксиоме присваивания. Получится предусловие 2*x < 15 (или x < 8). Поскольку x < 5 ⇒ x < 8, то спецификация программы верна. 2. Найти слабейшее предусловие для заданной программы if x < 0 then y := x + 1 else y := x - 1 и постусловия y > 0 15 Решение: согласно аксиоме условного оператора искомое предусловие можно выразить следующим образом. ( x < 0 → wp( y := x + 1 , y > 0 )) ∧ ( x ≥ 0 → wp( y := x - 1 , y > 0 )) далее можно выразить вложенные слабейшие предусловия, используя аксиому присваивания (игно- рируем области определения правых частей присваиваний), после чего искомое предусловие приоб- ретет следующий вид: ( x < 0 → x + 1 > 0 ) ∧ ( x ≥ 0 → x - 1 > 0 ) После эквивалентных логических преобразований последовательно получим: ( x ≥ 0 ∨ x > -1 ) ∧ ( x < 0 ∨ x > 1 ) ( -1 < x < 0 ) ∨ ( x > 1 ) Это и дает искомое слабейшее предусловие, в чем можно убедиться непосредственно. Действитель- но, при x < 0 необходимое постусловие y > 0 может быть получено после присваивания y := x + 1 только если x > -1 , а при x ≥ 0 то же постусловие может быть получено после присваивания y := x - 1 только при x > 1 3. Доказать, что верна следующая спецификация программы. x = N ∧ N > 0 { f := 1; while x > 0 do begin f := f * x; x := x – 1 end } f = N! Решение: покажем, что предикат I = {f=N!/x! ∧ x≥0} является инвариантом для основного цикла программы. Если это будет показано, то очевидно, что при окончании работы цикла требуе- мое постусловие будет истинным, поскольку I ∧ x≤0 эквивалентно f=N! ∧ x=0 , а из этого, оче- видно, следует заданное постусловие. Для того, чтобы доказать, что I является инвариантом цикла, надо показать, что I∧(x>0) {f := f * x; x := x – 1} I. Для этого воспользуемся аксиомой при- сваивания и аксиомой последовательного выполнения операторов и вычислим слабейшее предусловие wp(f := f * x; x := x – 1 , I ) . Применяя эти аксиомы, получим для слабейшего предусловия сле- дующее выражение: f*x=N!/(x–1)! ∧ x–1≥0 которое эквивалентно условию I∧(x>0) . Очевидно также, что цикл рано или поздно завершится, поскольку переменная x в теле цикла постоянно уменьшается. Тогда по теореме о цикле получаем, что условие I может служить предусловием для цикла. Подставляя в него вместо f значение 1, по- лучим условие 1=N!/x! ∧ x≥0 , эквивалентное условию x = N ∧ N ≥ 0 . Следовательно, заданная спецификация верна. 16 3. Теоретические модели вычислительных процессов. Взаимодействие и управление процессами Понятие "программа" – недостаточно мощное понятие для описания операционных систем, однако детальное иссле- дование программ позволяет выделить ряд важных концепций, которые проясняют принципы построения операционных систем. При выполнении программ явно выделяются три объекта: • последовательность команд или процедура, которая определяет программу; • процессор, который выполняет процедуру; • среда, т. е. та часть окружающего мира, которую процессор может непосредственно воспринимать или изме- нять. К среде относятся, например, память, универсальные и управляющие регистры ЭВМ, поскольку они могут и вос- приниматься, и изменяться программой. Можно выделить следующие свойства программы: • операции, заданные процедурой, выполняются строго последовательно, т. е. следующий шаг не начинает- ся, пока предыдущий полностью не завершится (из определения программы мы исключаем любой процесс, содержащий совмещение операций); • среда полностью управляется программой, а следовательно, и изменяется только в результате шагов, вы- полненных программой; • время выполнения операций, а также временной интервал между выполнением операций не имеют отно- шения к выполнению программы. Естественно, здесь мы не учитываем, что вся программа должна быть выполнена за ра- зумный интервал времени; • совершенно не имеет значения, выполняется ли программа целиком на одном процессоре, лишь бы не из- менялась среда программы. Программа в силу указанных свойств предполагает отсутствие внешнего воздействия на ее выполнение. Хорошим приближением такого рода программ являются программы, написанные на языках высокого уровня. Важное свойство таких программ – возможность точного повторения их работы, если только она не имеет доступа к часам реального времени. Программы, удовлетворяющие указанным свойствам, не могут быть операционными системами, ибо: • предполагается, что операционная система эффективно использует все ресурсы компьютера, а это требует со- вмещения операций различных компонент; • ОС отвечает на поступающие запросы за определенное время, а так как они поступают произвольным образом, то последовательность операций определяется не только самой системой. Важнейшей частью операционной системы, непосредственно влияющей на функционирование вы- числительной машины, является подсистема управления процессами. Процесс (или по-другому, задача) - абстракция, описывающая выполняющуюся программу. Для операционной системы процесс представляет собой единицу работы, заявку на потребление системных ресурсов. Подсистема управления процессами планирует выполнение процессов, то есть распределяет процессорное время между несколькими одновре- менно существующими в системе процессами, а также занимается созданием и уничтожением процессов, обеспечивает процессы необходимыми системными ресурсами, поддерживает взаимодействие между про- цессами. |