Некоммерческая организация «Ассоциация московских вузов»

Государственное образовательное учреждение

высшего профессионального образования

Московский государственный индустриальный университет

ГОУ ВПО МГИУ

Научно-образовательный материал

«Определение программ в терминах wp»

Состав научно-образовательного коллектива:

, к. т.н.

, ведущий инженер

Москва 2010 г.

Определение программ в терминах wp

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

Сейчас мы полностью изменим точку зрения. Будем считать первич­ным предикат wp и условия, которым он удовлетворяет. Это позволит нам определить в терминах wp семантику команд языка Ruby, а затем доказывать различные утверждения о программах.

Пустой оператор

Для пустого оператора определение выглядит так:

wp("",R) = R.

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

Оператор выхода

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

wp("exit", R) = F.

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

Последовательное выполнение

Следующее определение описывает результат последовательного выпол­нения двух операторов одного за другим:

НЕ нашли? Не то? Что вы ищете?

wp("Sl; S2",R) = wp("Sl",wp("S2", R)).

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

wp("x = e",R) = domain(e)lk&,Re,

где domain{e) — предикат, описывающий множество всех состояний, в которых может быть вычислено значение е (т. е., где е определено), a R^ обозначает подстановку в предикат R выражения е вместо всех свободных вхождений переменной х.

Замечание

1

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

Пример 1

wp("x = 5", х = 5) — (Т&&(5 = 5)) — Т, что вполне правильно, так как присваивание переменной х числа 5 всегда делает х равным пяти.

Пример 2

wp("x = 5", х ф 5) — (Т&&(5 ф 5)) = F, что тоже правильно, ибо присва­ивание переменной х числа 5 никогда не сможет сделать х ф 5.

Пример 3

wp("x = х + 1", х < 0) — (х + 1 < 0) — (х < — 1), где предикат domain(x + 1) опущен.

Пример 4 Здесь, наоборот, про domain(e) забывать нельзя: wp("x = 1/у",ж $С 0) = (уф0)кк(1/у^0) = (у<0).

Множественное присваивание

Пусть ж1, ж2 — переменные, a el, е2 — произвольные выражения. Введём обозначение domain(el}e2) = domain(el) Л domain(e2). Тогда

wp("xl, x2 = е1,е2",Я) = domain(el, e2)&&Rxel'^,

где Щх'е2 обозначает одновременную подстановку в предикат R выраже­ний el и е2 вместо всех свободных вхождений переменных xl и х2 соот­ветственно.

Пример

«ф("х, у = у, х", х = ЗАу = А) = (х = ЗАу = A)xyf = (у = ЗЛх = 4).

Ещё пример

Вычислите wp("х, у = х-у, у-х", х + у — с).

Решение

иф("х, у = х-у, у-х", х + у — с) = (х — у + у — х = с) — (с = 0).

Замечание

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

Массивы с функциональной точки зрения

Массив b [0. .п-1] можно считать простой переменной Ь, а «индексацию» его элементов (т. е. получение элемента b [i] по его индексу) — вызовом

2

метода [] массива b с параметром i. Именно так всё и «устроено на самом деле» в Ruby и многих других языках программирования.

Массивы и присваивание

По этой причине присваивание Mb[i] = е" элементу массива можно рас­сматривать, как простое присваивание "b = (b; i:e)". При этом будет использоваться следующее обозначение:

(h ■ л г - п J &Ы' если i ^ 3 I е, если г = j.

Присваивание элементу массива

Для массива Ь[0..п — 1] допустимыми значениями индекса принято считать диапазон [0..п — 1], хотя язык Ruby допускает и отрицательные величины (с особой трактовкой). Поэтому

iup("b[i] = e",i?) — inrange{b, i)hhdomain(e)hlkR{bi:e\,

где предикат inrange(b, г) определён так: inrange(b, i)=0^iAi<n.

Пример

тр(»Ы±1 = 5»,ЬИ = b[j}) = (ЬЩ = 6[i])^:5) = = ((Ь;г:5)[г] = (Ь;г:5)И) = = (г ф j Л 5 = b[j}) v (г = j Л 5 = 5) = = (г ^ i Л 5 = ЬЩ) V (г = j) = = (г ф j V г = j) Л (5 - ВД V г = j) = = Т Л (5 = ЬЩ V г = j) = (5 = ВД V г = j). Более сложный пример Найдите iup("b[b[i]] = i",b[i] = i).

Решение

wp("b[b[i]] = i",b[i] = i) =

= (b[i\ = i)Um) = ((b;b[i]:i)[i] = i) =

= ((b[i\ ф i A b[i] = i) V (b[i\ = г Л г = г) = = FV(b[H = i) = (6[г] = г).

Регулярные выражения

Точные определения будут даны намного позже (на 3-м курсе), но исполь­зовать это важное понятие мы начнём уже сейчас.

Сопоставление с образцом

Регулярные выражения (regular expressions) в языке Ruby являются объ­ектами типа Regexp и используются, например, в механизме сопоставле­ния с образцом (pattern matching).

Обычные и специальные символы Простейший способ задать регулярное выражение — использовать кон­струкцию /regexp/. Все символы, кроме., I, (, ), [, \, ",{,+,$,* и? представляют в регулярных выражениях самих себя. Для того чтобы включить в регулярное выражение один перечисленных специальных сим­волов, необходимо экранировать его с помощью символа \.

Значение специальных символов

Символ

Значение

\ $

Используется для экранирования

Любой символ, кроме ' \п'

Обязательно начало строки

Обязательно конец строки

Примеры

Выражение

Значение

/Маша/ /М. ша/

ЛМаша/

/лМаша$/

Слово Маша

Слово Маша, в котором вторая буква может быть заменена на любой символ

В строке Маша ела кашу это регулярное выра­жение содержится, а в строке Я Маша — нет Такое регулярное выражение будет обнаруже­но только в строке с единственным словом Маша (даже пробелы до или после него недопустимы)

Задание класса символов

Для определения класса символов применяется конструкция [characters], в которой почти все специальные символы становят­ся обычными. При этом знак - (минус) используется для задания диапазона; а символ " сразу после открывающей квадратной скобки означает операцию дополнения. Кроме того, используется ряд сокра­щений, среди которых \d = [0-9] (десятичные цифры), \D = [л0-9], \s = [\s\t\r\n\f] (пробельные символы), \S = ["As\t\r\n\f].

Примеры

Выражение /М[аи]ша/ /М[ла]ша/

/[l-9]\d/

Значение Слова Маша и Миша

Слово Маша, в котором вторая буква обязатель­но заменена на любой другой символ Десятичная запись чисел от 10 до 99

Сложные регулярные выражения

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

г*

ноль или более повторений г

г+

одно или более повторений г

r{m, n>

от т до п повторений г

r{m,}

не менее т повторений г

г?

ноль или одно повторение г

Примеры

Выражение

Значение

/[l-9]\d*/

Десятичная запись всех натуральных

чисел

/(Ma)+ша/

Слова Маша, МаМаша, МаМаМаша и так да-

лее

/~\s+M[an]iiia\s*$/

Строка, начинающаяся с как минимум

одного пробельного символа, за кото-

рым следует одно из слов Маша или Миша

и, возможно, другие пробельные симво-

лы

Языки и регулярные выражения

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

Задача 1 Опишите язык, задаваемый грамматикой G = (Е, TV, Р, S), где Е = {0,1}, N = {S, Т}, а множество правил Р таково:

S -> ОТ | IS Г -)• OS | IT Ответ 1

В данном случае язык пуст: L(G) = 0, поэтому использовать регулярные выражения нет необходимости.

Задача 2

S ->• ОТ | 15

Т ->• ОТ | г

Ответ 2

Язык L(G) представляется так (при использовании синтаксиса регуляр­ных выражений Ruby): /1*0+/, что часто записывают в виде 1*0+.

Задача 3 5 ->• 05 | ОТ Г ->• IT | г Ответ 3 L(G) = 0+1* или /0+1*/ в Ruby. Задача 4 5 ->• ОТ | ГО | 1 Т ->• 05 | 50 Ответ 4

В данном случае язык L(G) состоит из всех цепочек над алфавитом {0,1}, содержащих чётное число нулей и ровно одну единицу, которая может быть расположена на произвольной позиции. Он может быть задан пра-волинейной грамматикой

5 -> IT | 010Г | 005 Г -> 00Т | г и регулярным выражением

L(G) = (00)*(010 + 1)(00)* или /(00)*(010|1)(00)*/.

Управляющие конструкции языка Ruby

Операторы и выражения

В языках программирования различают операторы (statements) и вира-(expressions). Последние характеризуются тем, что возвращают значение.

Замечание 1

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

Замечание 2 В большинстве других языков программирования условные операторы и различные операторы циклов действительно являются операторами и не возвращают никакого значения. В Ruby же почти всё является выраже­нием!

Пример

i = gets. to_i

s = if i <= 2 then "мало"

elsif i < 10 then "много"

else "очень много"

end puts s

Условные операторы IF и UNLESS

В операторе if-then-elsif-then-else-end количество elsif-ветвей мо­жет быть любым, a else часть может отсутствовать. При этом ключевое слово then необходимо только в случае написания выражения, вычисляе­мого при некотором условии, на одной строке с ним.

Оператор unless-then-else-end является «отрицательной формой» оператора if-then-else-end.

Пример конструкции CASE

i = gets. to_i s = case i

when 0..2 then "мало"

when 3..9 then "много"

else "очень много"

end puts s

Ещё один пример

case gets. chop!

when "exit", "quit"

exit when /~\s*[l-9]\d*\s*$/

puts "Число" when /(\d*)\+(\d*)/

puts "#{$l. to_i+$2.to_i}" else

puts "Ошибка" end

Циклы WHILE и UNTIL

Как и условные операторы if и unless цикл while-end и его «отрица­тельная форма» until-end могут быть использованы в форме модифика­торов выражений. Вот пример «однострочника» (oneliner), печатающего количество введённых строк.

п = 0; п += 1 while gets; puts n

Итераторы

Циклы есть в большинстве языков программирования, но Ruby предоста­вляет ещё одну возможность — в нём есть итераторы. С их помощью написать правильную программу значительно легче.

3.times do puts "A" end

Примеры итераторов

(0..2).each do

puts "A" end

O. upto(3) do

puts "A" end

[1, 2, 3].each do

puts "A" end

2.downto(0) do ["А","Б","В"].each do

puts "A" puts "A"

end end

Итератор LOOP

Конструкция

loop {

# Блок операторов

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

Контрольные операторы

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

Конструкция

Действие

break redo

next retry

Прерывает выполнение цикла (итератора) Повторяет текущую итерацию с начала без пе­репроверки условия (для цикла) или повторной обработки текущего элемента (для итератора) Прерывает выполнение текущей итерации и на­чинает следующую

Повторяет выполнение цикла или итератора с самого начала

Пример

Следующая программа напечатает число 12.

i = 0

while i < 10 i = i + 1

next if i >= 12

redo if i >= 3 end puts i

Итератор FOR

В таких языках как Java, C++ и С, оператор for представляет собой модифицированный while, дополненный выражениями, выполняемыми до начала цикла и после каждой его итерации. В языке Ruby for является просто «синтаксическим сахаром», облегчающим написание итераторов определённого вида. Следующие две конструкции эквивалентны.

for i in list list. each do |i|

i. puts i. puts

end end

Управляющие конструкции в терминах wp

Замечание Основным условным оператором, имеющимся практически во всех языках программирования, является оператор IF. Оператор WHILE играет анало­гичную роль среди операторов цикла. Поэтому именно их мы и определим формально с помощью слабейшего предусловия, понимая под IF и WHILE следующие программы:

if е then SI while е

else S2 S

end end

Определение оператора IF

wp("IF", R) = domain(e)&,&,

(e =>■ wp("Sl",R)) A (!e => wp("S2",R)).

Пример

В качестве примера использования этого определения убедимся в том, что

wp("x >= у? z=x : z=y", z = тах(х, у)) = Т.

Решение

wp("x >= у? z=x : z=y",z = тах(х, у)) = (((х ^ у) =>- w;p("z=x", z = max(х, у)))А\(х ^ у) =>• "z=y",z = тах(х, у)) = (((х ^ у) =>■ (х = тах(х, у)))А\(х ^ у) =>■ (у = тах(х, у))) = ((!(# ^ у) V (х = тах(х, у)))Л\(\(х ^ г/)) V (у = тах(х, у))) = (((ж < г/) V (ж = тах(х, у))) А (х^у)У (у = тах(х, у))).

Продолжение решения

Покажем, что каждый из двух членов получившейся конъюнкции

(((х < у) V (х = тах(х, у))) Л (х ^ у) V (у = тах{х, у)))

является тавтологией.

Рассмотрим, например, первый из них — ((х < у)W(x = тах(х, у)). Если ж < ?/, то истинен первый дизъюнктивный член. В противном случае х ^ у и поэтому истинен её второй член.

Теорема об операторе IF

Пусть предикат Q удовлетворяет условию

((Q Л е) => wp(Sl, Д)) Л ((QA! e) =Ф wp(,S2, Л)).

Тогда (и только тогда)

Q =>■ wp("IF", R).

Вспомогательные определения

Hq(R) = domain{e)k,k,{\e A R),

Hk(R) = #fc_i(i2) V (domain(e)kkwp(S)Hk_l(R)))

Здесь предикат Hk(R) описывает множество всех состояний, в которых

выполнение цикла WHILE заканчивается не более, чем за к итераций, в

состоянии, удовлетворяющем R.

Определение оператора WHILE wp("miLE", R) = (Эк ^ 0Hk(R)). Пример Для цикла WHILE с условием продолжения i < 1 и телом i += 1 и посту­словия R = (г = 1) имеем Hq(R) = (г ^ 1Лг = 1) = (г = 1). Действительно, именно при таком предусловии выполнение цикла завершится за ноль ите­раций и даст результат R.

Далее, легко посчитать wp(" IF", H0(R)) = (г + 1 = 1) = (г = 0) и Ях(Л) = (г = 1) V (г < 1 Л г = 0) = (г = 1 V г = 0).

Аналогично находим Я2(Д) = (z = lVz = 0Vi = — 1) и т. д.

Итоговое замечание

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