В.Ш. Кауфман - Языки программирования - концепции и принципы (1990) (1160787), страница 60

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 60)

цикла, и попробуем вывести q(11). По правилу преодоления (П4) в точке (11)

выводимо

q(11)a :: x = max(M,i) & "not" (i < n ) .

Сразу ясно, что q(11) не выводимо из q(11)a. Легко построить

противоречащий пример:

i = 3, n = 2, M = (1,3,10); max (M,3) = 10.

Корректировка инварианта. Как видно, мы не зря сразу занялись задачей

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

его инвариант.

Контрпример получен при i > n. Ясно, что в цикле (3-11) такое значение

i получиться не может, он сохраняет условие i <= n. Но ведь это значит, что

обнаружен еще один претендент на роль инварианта цикла! Обозначим его через

I2.

I2 :: i <= n .

Нетрудно проверить, что соединяя I1 с I2 в утверждении

I3 :: I1 & I2

можно доказать q(11).

Проведем это доказательство.

Действительно, если I3 окажется инвариантом, то по правилу преодоления

цикла выводимо для точки (11)

q(11)b :: I1 & I2 & "not"(i < n) .

Но

q(11)b => (x = max(M,i) & (i = n) => x = max(M,n) .

Что и требовалось.

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

утверждения, претендующие на роль инварианта, приходится довольно часто в

процессе подбора оптимальных инвариантов. Поэтому полезно сформулировать

общее правило:

Конъюнкция инвариантов некоторого цикла остается инвариантом этого

цикла.

Обратное, естественно, неверно. (Приведите контрпример).

Это правило более общего характера, чем правила преодоления языка Д,

оно справедливо для любых инвариантов любого преодоления конструктов любого

ЯП.

Инвариантность I1 и I2. Опираясь на правило соединения инвариантов, мы

можем теперь решать задачу (а) отдельно для I1 и I2. Займемся сначала

доказательством инвариантности I2, как делом более простым.

Напомним, что доказать инвариантность I2 для цикла (3-11) - это значит

доказать истинность утверждения

Ak : {I2 & Pk} Sk {I2}

которое в нашем случае сводится к единственной тройке Хоара

{I2 & (i < n)} Ф(4-10) {I2}

так как в цикле (4-11) из п.15.2.3 лишь один вариант.

Чтобы вывести нужную тройку, начнем с утверждения

q(4)a :: I2 & (i < n) :: (i <= n) & (i < n)

как предусловия для Ф(4-11) и постараемся применить правила преодоления

сначала присваивания (4-5), а затем развилки (5-10) для вывода утверждения

q(10)a :: I2.

Но

q(4)a => (i < n)

и по правилу преодоления присваивания получаем

!=> (i <= n) :: q(5)a .

Аккуратный вывод q(5)a предоставляем читателю (достаточно подготовить

для Ф(4-5) предусловие в виде (Y = i+1) => (Y <= n) ).

Теперь одного взгляда на фрагмент (5-10) достаточно, чтобы убедиться,

что он сохраняет q(5)a - ведь он не изменяет ни i, ни n. Но это соображения

содержательные, а при формальном выводе несложно воспользоваться правилами

преодоления развилки и вложенных в него операторов (присваивания и пустого).

Оставим это в качестве упражнения и закончим тем самым доказательство

инвариантности I2.

Внешний инвариант. Полезно сформулировать в явном виде правила

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

преодолеваемых фрагментах. При этом мы, конечно, не получим принципиально

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

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

(разбив инвариант цикла на части и занимаясь ими по очереди).

Ясно, что упрощенное правило преодоления должно состоять в

переписывании предусловия в качестве (конъюнктивного члена) постусловия.

Назовем внешним инвариантом преодолеваемого фрагмента всякое

утверждение, к которому применимо такое упрощенное правило. Сформулировать

признаки внешних инвариантов для отдельных конструктов языка Д - полезное

упражнение.

Инвариантность I1. Вернемся к нашей программе-примеру и попытаемся

доказать, что I1 - инвариант цикла (3-11).

Нужно доказать утверждение

Ak : {I1 & Pk} Sk {I1}

т.е. в нашем случае

{x = max(M,i) & (i < n)} Ф(4-10) {x = max(M,i)} .

Обозначим I1 & (i < n) через q(4) и рассмотрим его как предусловие для

присваивания (4-5).

Преодолевая присваивание, получим

q(5) :: (x = max(M,i-1)) & (i-1 < n) .

Чтобы выполнить это преодоление аккуратно по правилам, нужно сначала

применить правило преодоления точки и получить

(Y = i+1) => (x = max(M,Y-1)) & (Y-1,n)

т.е. получить предусловие присваивания в удобной для преодоления форме,

а затем получить q(5) непосредственно по правилу (П1).

Теперь нужно преодолеть развилку (5-10).

В соответствии с правилом (П2) постусловие развилки должно быть

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

I1. Со второй ветвью развилки (5-10) никаких сложностей не возникает:

q(5) & (M[i] <= x) => (x = max(M,i)) :: I1 .

(Применено правило преодоления пустого оператора, т.е. обычное логическое

следование).

Займемся первой ветвью.

Ясно, что предусловие

q(6) :: q(5) & (M[i] > x)

непосредственно не пригодно для преодоления присваивания (6-7). Формально

потому, что зависит от x. Содержатольно потому, что связь "нового"

рассматриваемого значения массива, M[i], с остальными значениями

(проявляющаяся в том, что M[i] - максимальное из них) выражена неявно и к

тому же через значение x, которое "пропадает" в результате преодоления

присваивания. Так что наша ближайшая цель - в процессе подготовки к

преодолению проявить эту связь. Именно

q(6) => (M[i] = max(M,i) :: q(6)b .

Обозначив M[i] через Y, нетрудно теперь вывести I1 в качестве

постусловия первой ветви развилки (5-10), а следовательно и цикла (3-11).

Осталось убедиться, что I3 логически следует из q(3). Это очевидно.

Исключение переменных. Подчеркнем важность приема, примененного при

преодолении присваивания (6-7), его методологическое значение при

доказательстве свойств программ на основе дедуктивной семантики. Перед

преодолением операторов, содержательно влияющих на предусловие, необходимо

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

(т.е. найти инвариант). Назовем этот прием исключением переменных.

Получение подходящих следствий предусловия - творческий акт в

преодолении таких операторов. Методологическое значение приема исключения

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

Так что методика применения дедуктивной семантики для доказательства

корректности программ довольно тонко сочетает творческие содержательные

действия с чисто формальными.

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

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

рядом методических приемов, опирающихся на понимание сути этой программы.

Однако проверить корректность самого доказательства можно теперь чисто

формально, не привлекая никаких содержательных (а значит, и подозрительных

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

соответствующее формальное правило преодоления конструкта и проверять

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

Д и разработали элементы методики ее применения.

Вопрос. Могут ли в программе вычисления максимума остаться ошибки? Если

да, то какого характера?

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

характерные для взгляда на ЯП с математической позиции? Какие именно? Чем с

этой позиции отличаются методы Бэкуса и Хоара?

16. Реляционное программирование (модель Р)

16.1. Предпосылки

Основную идею классического операционного (процедурного) подхода к

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

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

способный учитывать параметры конкретной задачи. Записав этот алгоритм в

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

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

подходящими аргументами.

Итак, исходными понятиями операционного подхода служат:

класс задач;

универсальный алгоритм решения задач этого класса;

параметрическая процедура, представляющая этот алгоритм на выбранном

исполнителе;

вызов (конкретизация) этой процедуры с аргументами, характеризующими

конкретную задачу. Исполнение этого вызова и доставляет решение нужной

задачи.

[Конечно, это весьма упрощенная модель "операционного мышления".

Достаточно вспомнить, что, например, понятие параллелизма заставляет

отказаться от представления о единой процедуре, определяющей

последовательность действий исполнителя, и ввести понятие асинхронно

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

что каждый процесс остается по существу параметрической процедурой,

способной корректировать последовательность действий исполнителя в

зависимости от характеристик решаемой задачи. И не важно, передаются ли эти

характеристики в качестве аргументов при запуске процесса, извлекаются им

самостоятельно из программной среды или определяются при взаимодействии с

другими процессами.]

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

характеризующим класс задач, считается алгоритм (процедура) их решения.

Другими словами (в другой терминологии) можно сказать, что параметрический

алгоритм "представляет знания" об этом классе задач в процедурной (иногда

говорят "рецептурной") форме. Такие знания, в свою очередь, служат

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

знания уже о конкретной решаемой задаче.

Так что операционный подход требует представлять знания о классе задач

сразу в виде алгоритма их решения, позволяя абстрагироваться лишь от свойств

конкретной задачи. Между тем жизненный опыт подсказывает, что любой

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

о фактах, понятиях и соотношениях в той проблемной области, к которой

относится этот класс.

Например, прежде чем сочинять процедуру, способную вычислять список

всех племянников заданного человека, нужно знать, что такое "сестра",

"брат", "родитель" и т.п. Причем эти знания вовсе не обязаны быть

процедурными - они могут касаться вовсе не того, КАК вычислять, а,

например, того, ЧТО именно известно о потенциальных исходных данных и

результатах таких вычислений.

Такие знания часто называют "непроцедурными", желая подчеркнуть их

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

свойств такого рода знаний, то, заметив, что они касаются обычно фактов и

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

"логическими" или "реляционными" (от английского relation - отношение).

16.2. Ключевая идея

Важно заметить, что если бы удалось отделить реляционные знания от

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

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

решения задач. Ведь реляционное представление знаний о классе задач -

абстракция от способа (алгоритма, процедуры) решения этих задач (и,

следовательно, может обслуживать самые разнообразные такие способы).

Более того, возникает соблазн разработать универсальный способ решения

произвольных задач из некоторой предметной области, параметром которого

служит реляционное представление знаний об этой области.

Это и есть ключевая идея реляционного подхода. Другими словами, в этом

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

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

совершенно излишним. Программирование сводится к представлению релящионных

знаний о некоторой предметной области (например, о родственных отношениях

людей). Такое представление совместно с представлением данных о конкретной

Характеристики

Список файлов книги