рефераты конспекты курсовые дипломные лекции шпоры

Реферат Курсовая Конспект

Описание смысла программ

Описание смысла программ - раздел Программирование, Математические основы программирования. Теория схем программ. Семантическая теория программ Существует Несколько Причин, По Которым Следует Заниматься Описанием Семан...

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

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

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

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

2.1.1. Операционная семантика

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

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

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

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

Семантику конструкции for языка С можно описать в терминах следующих простых команд.

Пример 2.1. Оператор языка С Операционная семантика

for (expr1; expr2; ехргЗ){ exrp1

... loop: if expr2 = 0 gotoout

} …

ехргЗ;

gotoloop

out:

Человек, читающий подобное описание, является «виртуальным компьютером» и предполагается способным правильно «выполнить» команды описания и распознать эффект такого «выполнения».

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

ident := var

ident := ident - 1

goto label

if var relop var goto label

Здесь relop-одни из операторов отношений из набора {= , <>, >, <, >=, <=}, ident - идентификатор, a var - идентификатор или константа. Все эти операторы просты и легки для понимания и реализации.

Незначительное обобщение приведенных выше трех операторов присваивания позволяет описывать более общие арифметические выражения и операторы присваивания. Например:

ident := var bin_op var

ident := un_op var

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

Описание операционной семантики функций рассмотрим на примере системы равенств:

f1(x1, x2, ... , xk)= E1,

f2(x1, x2, ... , xk)= E2,

. . . . . . . . . . . . . (2.1)

fm(x1, x2, ... , xk)= Em,

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

Операционная семантика интерпретирует эти равенства как систему подстановок. Под подстановкой <s, E, t> терма t в выражение E вместо символа s (в частности, переменной) будем понимать переписывание выражения E с заменой каждого вхождения в него символа s на выражение t. Каждое равенство fi(x1, x2, ... , xk)= Ei задает в параметрической форме множество правил подстановок:

< x1, x2, ... , xk; fi(t1, t2, ... , tk) → Ei; t1, t2, ... , tk>

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

Интерпретация системы равенств (2.1) для получения значений определяемых функций в рамках операционной семантики производится следующим образом. Пусть задан набор входных данных (аргументов) d1, d2, ... , dk. На первом шаге осуществляется подстановка этих данных в левые и правые части равенств с выполнением там, где это возможно, предопределенных операций и с выписыванием получаемых в результате этого равенств. На каждом следующем шаге просматриваются правые части полученных равенств. Если правая часть является каким-либо значением, то оно и является значением функции, указанной в левой части этого равенства. В противном случае правая часть является выражением, содержащим вхождения каких-либо определяемых функций с теми или иными наборами аргументов. Если для такого вхождения соответствующая функция с данным набором аргументов имеется в левой части какого-либо из полученных равенств, то либо вместо этого вхождения подставляется вычисленное значение правой части этого равенства, либо не производится никаких изменений. В том же случае, если эта функция с данным набором аргументов не является левой частью никакого из полученных равенств, то формируется (и дописывается к имеющимся) новое равенство. Оно получается из исходного равенства для данной функций подстановкой в него вместо параметров указанных аргументов этой функции. Такие шаги осуществляются до тех пор, пока все определяемые функции не будут иметь вычисленные значения.

Пример 2.2. Рассмотрим систему равенств, определяющую функцию FACT(n)=n!

FACT(0)=1,

FACT(n)=n´FACT(n-1).

Для вычисления значения FACT(3) осуществляются следующие 6 шагов.

1-й шаг: 2-й шаг: 3-й шаг:

FACT(0)=1, FACT(0)=1, FACT(0)=1,

FACT(3)=3´FACT(2). FACT(3)=3´FACT(2), FACT(3)=3´FACT(2)

 FACT(2)=2´FACT(1). FACT(2)=2´FACT(1),

FACT(1)=1´FACT(0).

4-й шаг: 5-й шаг: 6-й шаг:

FACT(0)=1, FACT(0)=1, FACT(0)=1,

FACT(3)=3´FACT(2), FACT(3)=3´FACT(2), FACT(3)=6,

FACT(2)=2´FACT(1), FACT(2)=2, FACT(2)=2,

FACT(1)=1. FACT(1)=1. FACT(1)=1.

Первым и самым значительным использованием формальной операционной семантики было описание семантики языка PL/I. Эта абстрактная машина и правила трансляции языка PL/I были названы общим именем Vienna Definition Language (VDL) в честь города, в котором они были созданы корпорацией IBM.

Операционная семантика является эффективной до тех пор, пока описание языка остается простым и неформальным. К сожалению, описание VDL языка PL/I настолько сложно, что практическим целям оно фактически не служит.

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

2.1.2. Аксиоматическая семантика

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

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

Аксиоматическая семантика основана на математической логике. Будем называть предикат, помещенный в программу утверждением. Утверждение, непосредственно предшествующее оператору программы, описывает ограничения, наложенные на переменные в данном месте программы. Утверждение, следующее непосредственно за оператором программы, описывает новые ограничения на те же (а возможно, и другие) переменные после выполнения оператора.

Введем обозначение (триада Хоара)

{Q} S {R}, (2.2)

где Q, R - предикаты, S - программа (оператор или последовательность операторов). Обозначение определяет следующий смысл: «Если выполнение S началось в состоянии, удовлетворяющем Q, то имеется гарантия, что оно завершится через конечное время в состоянии, удовлетворяющем R».

Предикат Q называется предусловием или входным утверждением S, предикат R - постусловием или выходным утверждением. Следовательно, R определяет то, что нужно установить. Можно сказать, что R определяет спецификацию задачи. В предусловии Q нужно отражать тот факт, что входные переменные получили начальные значения.

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

Пример 2.3. Рассмотрим оператор присваивания для целочисленных переменных и постусловие:

sum := 2 * х + 1 {sum > 1}

Одним из возможных предусловий данного оператора может быть {х > 10}.

Слабейшими предусловиями называются наименьшие предусловия, обеспечивающие выполнение соответствующего постусловия. Например, для приведенного выше оператора и его постусловия предусловия {х > 10}, {х > 50} и {х > 1000} являются правильными. Слабейшим из всех предусловий в данном случае будет {х > 0}.

– Конец работы –

Эта тема принадлежит разделу:

Математические основы программирования. Теория схем программ. Семантическая теория программ

Следуя А П Ершову мы употребляем термин теоретическое программирование в качестве названия математической дисциплины изучающей синтаксические.. В настоящее время сложились следующие основные направления исследований.. Математические основы программирования Основная цель исследований развитие математического аппарата..

Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ: Описание смысла программ

Что будем делать с полученным материалом:

Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:

Все темы данного раздела:

Программа как формализованное описание процесса обработки данных
Целью программирования является описание процессов обработки данных (в дальнейшем - просто процессов). Данные - это представление фактов и идей в формализованном виде, пригодном для п

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

Стандартные схемы программ
1.2.1. Базис класса стандартных схем программ Стандартные схемы программ (ССП) характеризуются базисом и структурой схемы. Базис класса фиксирует символы, из которых строятся схем

Свойства и виды стандартных схем программ
1.3.1. Эквивалентность, тотальность, пустота, свобода ССП S в базисе В тотальна (пуста), если для любой интерпретации I базиса В программа (S, I) останавливается (зацикливает

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

Рекурсивные схемы
1.5.1. Рекурсивное программирование Среди упомянутых выше методов формализации понятия вычислимой функции метод Тьюринга — Поста основан на уточнении понятия процесса вычислений, для чего

Трансляция схем программ
1.6.1. О сравнении класс сов схем. Программы для ЭВМ, будь-то программы, записанные на операторном языке, или программы на рекурсивном языке, универсальны в том смысле, что любую вычислиму

Обогащенные и структурированные схемы
1.7.1 Классы обогащенных схем Выделяют следующие классы обогащенных схем: класс счетчиковых схем, класс магазинных схем, класс схем с массивами. Классы счетчиковых и магази

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

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

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

Правила верификации К. Хоара.
Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желае

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

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

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

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

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

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

Then begin
X1:=X1*Y; end; X2:=X2*Y; Y:=Y-1; end; write(X1); write(X2); endРисунок 4.5.

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

Хотите получать на электронную почту самые свежие новости?
Education Insider Sample
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
Реклама
Соответствующий теме материал
  • Похожее
  • Популярное
  • Облако тегов
  • Здесь
  • Временно
  • Пусто
Теги