Информатика - Лекции - Семестр 2

Языки программирования высокого уровня

Синтаксис, формальные грамматики.

Для представления алгоритмов, предназначенных для выполнения на ЭВМ, используются языки программирования (ЯП). Внешняя форма программы на ЯП устанавливается с помощью синтаксиса языка , который определяет формальный язык. Он определяется с помощью определенных грамматических правил, аналогичных алгоритму текстовых подстановок. Основой формального определения синтаксиса являются формальные грамматики.

Синтаксис языка — это набор правил, определяющих допустимые конструкции языка. Синтаксис определяет «форму языка» — задает набор цепочек символов, которые принадлежат языку.

Семантика языка — это раздел языка, определяющий значение предложений языка. Семантика определяет «содержание языка» — задает смысловое значение для всех допустимых цепочек языка.

Грамматика — это описание способа построения предложений некоторого языка. Иными словами, грамматика — это математическая система, определяющая язык.

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

Правило — это упорядоченная пара цепочек символов (α, β). В правилах очень важен порядок цепочек, поэтому их чаще записывают в виде α→β.

Формально грамматика G определяется как четверка (N, T, P, S), где

•N — конечное множество нетерминальных символов или нетерминалов;

•T — конечное множество терминальных символов или терминалов, причем

N∩T= ;

•P — конечное множество правил грамматики вида α→β,

где (α , β) (N UT )* N(N UT )* ×(N UT )* .

•S — символ из N, называемый начальным символом.

Множество V = N T называют полным алфавитом грамматики G.

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

Пример 1.

Дана грамматика G =({A, S}, {0, 1}, P, S), где P = {S→0A1, 0A→00A1, A→e}.

Нетерминальными символами являются A, S, а терминальными 0, 1.

Грамматика определяет язык рекурсивным образом посредством задания особого рода выводимых цепочек.

Выводимые цепочки грамматики G = (N, T, P, S) определяются следующим образом:

•S — выводимая цепочка;

•Если αβγ — выводимая цепочка, и β→δ содержится в Р, то αδγ - тоже выводимая цепочка

Выводимая цепочка грамматики G, не содержащая нетерминальных символов,

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

Язык, порождаемый грамматикой G (L(G)) - это множество терминальных цепочек, порождаемых грамматикой G.

Пусть G = (N, T, P, S) — грамматика, V = N T — ее алфавит. α,β,γ V*, δ

V+. Цепочка ϕ = αβγ называется непосредственно выводимой из ψ = αδγ в

грамматике G, если в G существует правило δ→β P. Обозначается ψ G ϕ. В тех случаях, когда из контекста ясно, о какой грамматике идет речь, нижний индекс G будем опускать.

Иными словами, цепочка ϕ непосредственно выводима из ψ, если можно взять несколько символов в цепочке ψ, заменить их на другие символы согласно правилу грамматики и получить цепочку ϕ. Любая из цепочек δ и β (или обе они) может быть пустой. В предельном случае вся цепочка ψ может быть заменена на цепочку ϕ, тогда в грамматике G должно существовать правило ψ→ϕ P.

Через k будем обозначать k-ю степень отношения . Иначе говоря, α kβ , если существует последовательность α0,α1, α2,…, αk, состоящая из k+1 не обязательно различных цепочек, для которых α=α0, αi-1 αI, 1≤i≤k и αk=β. Эта последовательность называется выводом длины k цепочки β из цепочки α в

Говорят, что цепочка ψ выводима из ϕ (обозначение ϕ *ψ)тогда и только тогда, когда ϕ iψ для некоторого i≥0.

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

вывод называется законченным, если цепочка ϕ пустая или содержит только терминальные символы грамматики G = (N, T, P, S). Цепочка, полученная в результате законченного вывода, называется конечной цепочкой вывода.

Грамматики можно классифицировать по виду их правил. Грамматика G = (N, T, P, S) называется

•праволинейной, если каждое правило из Р имеет вид A→αB или A→α, где

A,B N, α V*;

•контекстно-свободной (бесконтекстной), если каждое правило из Р имеет вид A→α, где A N, α V*;

•контекстно-зависимой (неукорачивающей), если каждое правило из Р имеет вид α→β, где α ≤ β .

Грамматика, не удовлетворяющая ни одному из указанных ограничений,

называется грамматикой общего вида или грамматикой без ограничений.

Пример 2.

Праволинейная грамматика G1=({S}, {0, 1}, {S→0S|1S|e},S) порождает язык

L(G1)={0,1}*.

Пример 3.

Пусть G2=({E, T, F}, {a, +, *, (, )}, P, E), где Р состоит из правил

E→E+T|T

T→T*F|F

F→(E)|a

Язык L(G2) представляет собой множество арифметических выражений, построенных из символов a, +, *, (, ). Грамматика G2 — контекстно-свободная.

Пример 4.

Пусть G3=({C, B, S}, {a, b, c}, P, S), где Р состоит из правил

S→aSBC|abC

CB→BC bB→bb bC→bc cC→cc

Эта грамматика порождает язык {anbncn| n≥1}.Очевидно, это контекстнозависимая грамматика.

Для записи синтаксиса конструкций языков программирования часто используют форму Бэкуса-Наура. Она практически ничем не отличается от нотаций продукций

формальных грамматик, только вместо знака → используется обозначение ::=. Пример 5. Десятичное целое без знака. <Десятичное_целое_без_знака>::=<Цифра>|<Десятичное_целое_без_знака><Цифра> <Цифра>::=0|1|2|3|4|5|6|7|8|9

Семантика.

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

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

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

а также часто используемые методы композиции решений подзадач.

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

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

P

Q

Рис 3.1.

Здесь S — оператор, группа операторов или программа; Р — предусловие — логическое выражение, которое должно быть истинным перед выполнением S; Q — постусловие — логическое выражение, которое должно принимать истинное значение при выходе из вычислений S. Если ввести в язык понятие комментария как произвольного текста, заключенного в фигурные скобки, то свойство, изображенного на рис 3.1. можно в тексте программы записать как:

Это — спецификация программы S со следующим смыслом: если соотношение Р истинно перед выполнением S, то Q будет истинно после выполнения S.

Пусть Р некоторое логическое выражение. Для простоты будем полагать, что кванторы всеобщности и существования не принадлежат Р. Для выражения x(P)

считаем, что вхождение переменной х в x связано квантором всеобщности и каждое вхождение х в Р –связанное значение. Та же терминология применяется к

выражению x(P) , за исключением того, что в этом случае вхождение переменной

переменной этого выражения.

Пример 1

• все переменные в выражении ¬ x( y( y ≤ x)) связаны;

•все переменные в выражении (i < j) = ( j < k) свободны.

Определим понятие подстановки.

Пусть P - логическое выражение. Нотация

обозначает одновременную подстановку вместо всех свободных вхождений любой переменной xi в P соответствующего выражения yi. Вхождения xi в некоторые yi не замещаются. Переменные x1...xn должны быть различными, в противном случае подстановка не определена.

Пример 2.

(z =10)zx+y = (x + y =10)

(x + x + y)ax,+yb,c = a +b +a +b +c (x + x + y)xx,+yy,z = x + y + x + y + z

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

Если H1,…,Hn — истинные утверждения, то H — также истинное утверждение. Рассмотрим правила вывода для простых операторов языка программирования.

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

Он не оказывает никакого воздействия на значения программных переменных. Для любого P имеем правило вывода

Оператор присваивания

Он имеет вид x = e и устанавливает значение переменной x равным значению выражения e. Тогда для любого P

Пример 3.

{x+y=10} z:=x+y {z=10} {x-y>0} x:=x-y {x>0}

Рассмотрим правила вывода для более сложных конструкций - составных и условных операторов.

Составной оператор

Он образуется путем последовательной композиции операторов S1; S2;…;Sn. Знак ; используется для соединения операторов в последовательность. В модельном языке составной оператор (или блок операторов) представлен программной конструкцией:

Правило вывода для составного оператора имеет вид:

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

Селективный оператор выбора

Оператор Case выбирает для выполнения тот оператор-компоненту, метка которого ki совпадает с текущим значением селектора x. Если такой метки не обнаружено, то действие оператора (16) не определено. Очевидно, если требуется, чтобы Q было справедливым независимо от того, какой оператор Si выбирается для выполнения, мы имеем набор соотношений:

Тогда правило вывода для оператора выбора должно иметь вид:

заканчивается, когда В становится ложным. Определим правило вывода для этого оператора. Если Р - его предусловие, то предусловие для оператора S имеет вид

P B. Для итерационного повторения выполнения оператора S в цикле его постусловие должно совпадать с P. Следовательно, оператор S должен удовлетворять соотношению

{P B} S {P}

Оператор цикла с предусловием завершит свою работу, если справедливо

P¬B

Итак, получаем следующее правило вывода для оператора с предусловием

(17)

{P B} S {P}

{P} While B S Wend {P}

Далее будем называть Р инвариантом цикла.

Пример 6.

Рассмотрим оператор цикла

While r >= y

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

Wend

в предположении, что {x≥0 y>0}. Покажем, что данный цикл имеет инвариант

x=q*y+r 0≤r

Согласно правилам вывода для оператора присваивания и составного оператора легко получаем соотношение

{x=q*y+r 0≤r-y} r:=r-y; q:=q+1 {x=q*y+r 0≤r}

Предусловие составного оператора имеет форму P B. Поэтому для рассматриваемого цикла справедливо согласно (20) соотношение:

Где S – оператор (составной) и B - булево выражение. Здесь S выполняется перед вычислением B. Затем, если В ложно, процесс итерационного выполнения S продолжается, в противном случае он завершается.

Предположим, доказано, что {P} S {Q} и Q¬B P. Тогда возможно повторное

выполнение оператора S. Выход из цикла влечет за собой условие Q B. Тогда правило вывода для цикла с постусловием имеет вид

(22)

{P}S{Q}, Q (¬B P)

{P} Do S Loop Until B {Q B}

Пример 7.

Пусть дан цикл с постусловием

Do

z := z+y; u := u-1

Loop Until u = 0

Предположим, что x, y — переменные целого типа, которые удовлетворяют

условию x>0 y>0. Пусть требуемое постусловие цикла есть {z=x*y}. Очевидно, если объединить его с условием завершения цикла u=0, то его можно переписать в виде z+u*y=x*y. Используя правила вывода для операторов присваивания и составного оператора “z=z+y u=u-1” легко показать, что он имеет предусловие и постусловие {z+u*y=x*y}. Отсюда легко получить числитель правила вывода (22):

{z+u*y=x*y} z := z+y; u := u-1 {z+u*y=x*y}, {z+u*y=x*y} u>0

Отсюда и из правила вывода (22) следует, что

{z+u*y=x*y} z := z+y; u := u-1 {{z+u*y=x*y} u=0}

Очевидно, полученное постусловие эквивалентно {z=x*y}. Следует обратить внимание, что неявно мы здесь воспользовались еще одной группой правил вывода - правилами консеквенции.

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

Корректность программ.

Правильность программ обычно проверяется тестированием. Оно заключается в том, что выбираются конкретные значения входных данных программы и программа выполняется с этим входными данными. Результаты работы программы сравниваются с заранее известными правильными результатами.

Тестирование - процесс выполнения программы с намерением найти ошибку. Но оно никогда не докажет их отсутствия. Поэтому необходимо абстрагироваться от

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

Пример 1.

Алгоритм деления целых неотрицательных чисел x на у. Результат операции частное q и остаток r, которые удовлетворяют соотношению

x=q*y+r 0≤r<y

Очевидно, это постусловие программы, ее предусловие имеет вид x≥0 y>0

Алгоритм можно записать следующим образом

‘{x≥0 y>0} q = 0

r = x

‘{x=q*y+r 0≤r}

While r>=y

‘{x=q*y+r 0≤y<r} r = r-y

q = q-1 Wend

‘{x=q*y+r 0≤r<y}

Заметим, что первые два оператора q=0 и r=x автоматически гарантируют

истинность инварианта цикла {x=q*y+r 0≤r}. Этот типичный прием называется

инициализацией инвариантов цикла.

В примере 5 предыдущего параграфа мы доказали, что для цикла справедливо правило

‘{(x=q*y+r) 0≤r} While r>=y

r=r-y q=1+q

Wend

‘{(x=q*y+r) 0≤r<y}

Так как программный составной оператор состоит из операторов инициализации цикла и данного оператора цикла, то по правилу вывода для составного

оператора получаем постусловие программы {(x=q*y+r) 0≤r<y}, что и требовалось доказать.

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

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

2.Повторить этот процесс "декомпозиции и доказательство корректности декомпозиции" для подзадач.

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

Проиллюстрируем этот метод проектирования сверху вниз на простом примере.

Пример 2.

Умножение двух положительных целых чисел x и y. Результат – z. Начальное описание алгоритма таково:

‘{x>0 y>0}

‘сложить значение у само с собой x раз

‘ {z=x*y}

Предусловие есть требование положительности х и у. Постусловие - результат вычислений. Правильность преобразования предусловия в постусловие следует из определения операции сложения.

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

1.

‘{x>0 y>0}

Установить z равным нулю, u равным x

‘{z+u*y=x*y u>0}

2.

‘{z+u*y=x*y u>0}

‘Увеличить z на величину y и уменьшить u на 1; повторять этот процесс до тех ‘пор пока u не станет равным 0

{z=x*y}

Нетрудно заметить, что инвариантом является логическое выражение z+u*y=x*y

Тогда подзадача 1 содержит операторы присваивания, инициализирующие этот инвариант.

Действие «увеличить z на величину y и уменьшить u на 1» подзадачи 2

построено таким образом, чтобы сохранить инвариант. В самом деле, Z+y+(u-1)*y=z+u*y=x*y

Условие «повторять этот процесс до тех пор, пока u не станет равным 0»,

гарантирует, что после окончания итераций будет получен требуемый результат z=x*y.

Корректность подзадач показана, и мы получаем программу

‘{x>0 y>0} z = 0

u = x Do

z = z+y u = u-1

Loop until u=0

‘{z=x*y}

Можно непосредственно доказать корректность этой программы.

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