1611678431-0e68e83522cb9d960ac896aa5d90854d (826635), страница 16

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

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

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

В том же случае, если эта функция с данным набором аргументов не является левой частьюникакого из полученных равенств, то формируется (и дописывается к имеющимся) новое равенство. Онополучается из исходного равенства для данной функций подстановкой в него вместо параметров указанныхаргументов этой функции. Такие шаги осуществляются до тех пор, пока все определяемые функции не будутиметь вычисленные значения.Пример. Рассмотрим систему равенств, определяющую функцию FACT  n   n !FACT  0   1FACT  n   n  FACT  n  1 .Для вычисления значения FACT  3 осуществляются 6 шагов.шаг 1FACT  0   1FACT  3  3  FACTшаг 4FACT  0   1FACT  3  3  FACTFACT  2   2  FACTFACT 1  1221шаг 2FACT  0   1FACT  3  3  FACTFACT  2   2  FACTшаг 5FACT  0   1FACT  3  3  FACTFACT  2   2FACT 1  1212шаг 3FACT  0   1FACT  3  3  FACT 2FACT  2   2  FACT 1FACT 1  1 FACT 0шаг 6FACT  0   1FACT  3  6FACT  2   2FACT 1  1Операционная семантика является эффективной до тех пор, пока описание языка остается простым инеформальным.

Операционная семантика зависит от алгоритмов, а не от математики. Операторы одного языкапрограммирования описываются в терминах операторов другого языка программирования, имеющего болеенизкий уровень. Этот подход может привести к порочному кругу, когда концепции неявно выражаются черезсамих себя.2.3 Аксиоматическая семантикаАксиоматическая семантика была создана в процессе разработки метода доказательстваправильности программ. Семантику каждой синтаксической конструкции языка можно определить как некийнабор аксиом или правил вывода, который можно использовать для вывода результатов выполнения этойконструкции. Чтобы понять смысл всей программы, эти аксиомы и правила вывода следует использовать также, как при доказательстве обычных математических теорем.

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

То есть, доказано, что выходныеданные представляют значения соответствующей функции, вычисленной по значениям входных данных.Такие доказательства показывают, что программа выполняет вычисления, описанные ееспецификацией. В доказательстве каждый оператор программы сопровождается предшествующим ипоследующим логическими выражениями, устанавливающими ограничения на переменные в программе. Этивыражения используются для определения смысла оператора вместо полного описания состояния абстрактноймашины.Аксиоматическая семантика основана на математической логике.

Будем называть предикат,помещенный в программу утверждением. Утверждение, непосредственно предшествующее операторупрограммы, описывает ограничения, наложенные на переменные в данном месте программы. Утверждение,следующее непосредственно за оператором программы, описывает новые ограничения на те же (а возможно, идругие) переменные после выполнения оператора.Введем обозначение (триада Хоара)Q S Rгде Q, R - предикаты, S - программа (оператор или последовательность операторов). Обозначениеопределяет следующий смысл: «Если выполнение S началось в состоянии, удовлетворяющем Q , то имеетсягарантия, что оно завершится через конечное время в состоянии, удовлетворяющем R ».Предикат Q называется предусловием или входным утверждением S , предикат R - постусловием иливыходным утверждением, R определяет то, что нужно установить ( R определяет спецификацию задачи).

Впредусловии Q нужно отражать тот факт, что входные переменные получили начальные значения.Пример. Рассмотрим оператор присваивания для целочисленных переменных и постусловие:sum:=2*х+1 {sum>1}Одним из возможных предусловий данного оператора может быть {х>10}.Слабейшими предусловиями называются наименьшие предусловия, обеспечивающие выполнениесоответствующего постусловия. Например, для приведенного выше оператора и его постусловия предусловия{х>10}, {х>50} и {х>1000} являются правильными. Слабейшим из всех предусловий в данном случае будет{х>0}.2.3.1 Преобразователь предикатов.Э.

Дейкстра рассматривает слабейшие предусловия, т. е. предусловия, необходимые и достаточные длягарантии желаемого результата.«Условие, характеризующее множество всех начальных состояний, при которых запуск обязательноприведет к событию правильного завершения, причем система останется в конечном состоянии,удовлетворяющем заданному постусловию, называется слабейшим предусловием, соответствующим этомупостусловию».Если S - некоторый оператор (последовательность операторов), R - желаемое постусловие, тосоответствующее слабейшее предусловие будем обозначать wp  S , R  . Аббревиатура wp определяетсяначальными буквами английских слов weakest (слабейший) и precondition (предусловие).Определение семантики оператора дается в виде правила, описывающего, как для любого заданногопостусловия R можно вывести соответствующее слабейшее предусловие wp  S , R  .Для фиксированного оператора S такое правило, которое по заданному предикату R вырабатываетпредикат wp  S , R  , называется «преобразователем предикатов»:  wp  S , R  S R .Это значит, что описание семантики оператора S представимо с помощью преобразователяпредикатов.

Применительно к конкретным S и R часто бывает неважным точный вид wp  S , R  , бываетдостаточно более сильного условия Q , т. е. условия, для которого можно доказать, что утверждениеQ  wp  S , R  справедливо для всех состояний. Значит, множество состояний, для которых Q - истина, являетсяподмножеством того множества состояний, для которых wp  S , R  - истина.

Возможность работать спредусловиями Q , не являющимися слабейшими, полезна, поскольку выводить wp  S , R  явно не всегдапрактично.Сформулируем свойства wp  S , R  .1) wp  S , F   F для любого S . (Закон исключенного чуда).2) Закон монотонности. Для любого S и предикатов P и R таких, что P  R для всех состояний,справедливо для всех состояний wp  S , P   wp  S , R  .3) Дистрибутивностьконъюнкции.ДлялюбыхсправедливоS , R, Pwp  S , P  AND wp  S , R   wp  S , P AND R  .4) Дистрибутивность дизъюнкции.

Для любых S , R, P справедливоwp  S , P  OR wp  S , R   wp  S , P OR R  .Если для каждого оператора языка по заданным постусловиям можно вычислить слабейшеепредусловие, то для программ на данном языке может быть построено корректное доказательство.Доказательство начинается с использования результатов, которые надо получить при выполнении программы, вкачестве постусловия последнего оператора программы, и выполняется с помощью отслеживания программыот конца к началу с последовательным вычислением слабейших предусловий для каждого оператора. Придостижении начала программы первое ее предусловие отражает условия, при которых программа вычислиттребуемые результаты.Для некоторых операторов программы вычисление слабейшего предусловия на основе оператора иего постусловия является достаточно простым и может быть задано с помощью аксиомы.

Однако, как правило,слабейшее предусловие вычисляется только с помощью правила логического вывода, т. е. метода выведенияистинности одного утверждения на основе значений остальных утверждений.2.3.2 Аксиоматическое определение операторов языка программированияОпределим слабейшее предусловие для основных операторов: оператора присваивания, составногооператора, оператора выбора и оператора цикла.Оператор присваивания имеет вид: x : E , где x - простая переменная, E – выражение.Слабейшее предусловие оператора присваивания Q  wp  x : E , R  , получается из R заменой каждоговхождения x на E  Q  REx  .Предполагается, что значение E определено, и вычисление выражения E не может изменить значенияни одной переменной.

Следовательно, можно использовать обычные свойства выражений такие, какассоциативность, коммутативность и логические законы.Составной оператор имеет вид: begin S1;S2;... ;Sn end.Слабейшее предусловие для последовательности двух операторов:wp  S1 ; S 2 , R   wp  S1 , wp  S 2 , R   .Аналогично слабейшее предусловие определяется для последовательности из n операторов.Оператор выбора определяется:if B1  S1  B2  S2   Bn  Sn fi .Здесь n  0 , B1 , B2 , , Bn - логические выражения, называемые охранами, S1 , S2 , , Sn - операторы, параBi  Si называется охраняемой командой,  - разделитель, if и fi играют роль операторных скобок.Выполняется оператор следующим образом.Проверяются все Bi .

Если одна из охран не определена, то происходит аварийное завершение. Далее,по крайней мере, одна из охран должна иметь значение истина, иначе выполнение завершается аварийно.Выбирается одна из охраняемых команд Bi  Si у которой значение Bi истина, и выполняется Si .Слабейшее предусловие для этого оператора:wp  if , R   BB AND  B1  wp  S1 , R   AND…AND  Bn  wp  S n , R   , где BB  B1 OR B2 OR …OR Bn .Естественно определить wp  if , R  с помощью кванторов:wp  if , R     i :1  i  n : Bi  AND   i :1  i  n : Bi  wp  Si , R  Пример. Определить z  x .С использованием оператора выбора:if x  0  z : x  x  0  z :  x fi .К особенностям оператора выбора следует отнести, во-первых, тот факт, что он включает условныйоператор (if...then..), альтернативный оператор (if… then...

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

Список файлов ответов (шпаргалок)