Т. Пратт, М. Зелковиц - Языки программирования - разработка и реализация (4-е издание_ 2002) (1160801), страница 47
Текст из файла (страница 47)
Элемент 1ег х я- а тп Ьот)у 4.2. Семантика языка 167 используется для обозначения ((х): Ьо()у) (а ) и имеет тот же смысл, что и Х-выражение (Лх Ьопу а) Если х принадлежит к типу области () — а 0', то выражение х[ч!е) определяется как х(ч(е) = (О О) 0' : чт О = ч гпеп е е1ае х(Ь) Интуитивно понятно, что смысл этого выражения заключается в замене компонента ч элемента х компонентом е и представляет собой базоную модель операции присваивания.
Семантика операторов Теперь мы рассмотрим семантическое определение для каждого оператора нашего языка в терминах трансформаций (преобразований) состояний программы. Ъефп оператор еп((: последовательность ключевых слов Ьер1п ... епо не оказывает влияния на внутреннее состояние программы, то есть она является истинно тождественной функцией в пространстве состояний. Это можно представить как С((оец1п агпг епо)) - Ц (аггг]) сон(роз(аоп (композиция): в данном случае нам хотелось бы применить к некоторому состоянию последовательно два оператора; зг(пг1 и зг(агь Мы можем представить это как суперпознцию функций: Ц (агпг1; агвг2)) - (агаге а)агаге : С((агпг2))(С((агягп )(а)) Аргументом функции С( (зг(ага) ) является состояние, получившееся в резулътате выполнения оператора эг(пгь аэяяпшепг (присваивание): оператор присваивания создает новое отображение памяти, используя значение, полученное при вычислении выражения ехр в текушем состоянии: С((10 ч- ехр)) - (агаге а)агаге : ((ча1ое ч)агаге : а(14/ч)>(Е((ехр))(а)) 11 (ветвление): этот оператор определяет, какую из двух функций следует вычислить, причем сначала вычисляется значение функции Е при заданном выражении в качестве аргумента, полученное значение передается в качестве аргумента булевой функции, а затем уже вычисляется соответственно оператор ага(11 или оператор згяг,: С((М ехр гпеп агяг1 е1ае агпг2))- (агаге а)агаге : ((ьоо1 ы ага(а -+ агаге .
(1Г Ь гпеп С(( агпг1)))е1ае С((агяг2)))(Е((ехр)](а)1(а) ччЪ((е (цинл): определение этого оператора неизбежно получается рекурсивным (гес), так как функция ч(Ь1 1е сама является частью определения: с((чп11е ехр оо агап)- гес(агаге а)агаге : ((Ьао1 Ь)агаге -+агаге : (1Г Ь гьап С((агвг))*С((чп11е ехр с$о агвг))) е1ае ((агаге а')агаге , а')) (Е((ехр))(а))(а) заметим, что в принеденном определении для с((иь11е) ) мы действительно используем с((ч(ь1)е) ) в его же определении (как часть выражения гьеп), это объяс- 168 Глава 4.
Моделирование свойств языка ляется членом тес, обозначающим рекурсию (гесигз1те). Таким образом, наше определение иМ1е в действительности представляется в виде С((ящ !е)) - т(С((яю )е))) Это утверждение можно сформулировать проще: оператор ил11е является решением уравнения вида х= ((х). Такие решения называются неподвижнььии томками, и все, что нам нужно,— это наименьшая из всех неподвижных точек, которые решают это уравнение. Полный анализ теории неподвижных точек пе входит в задачу авторов книги. Однако мы надеемся, что приведенные в этой главе материалы дают некоторое представление о том, как системы, подобные ) -исчислению, могут быть расширены для моделирования языков программирования. 4.2.3.
Обзор языка М~ История, Язык МЕ (МегаЬапйпайе) является аппликативным языком, программы на этом языке пишутся примерна так же, как на языке С или Рааса!. Однако это аппликативный язык с улучшенной концепцией типов ланных. М1. поддерживает полиморфизм и, с помощью своей системы типов, абстракции данпьпс Основные структуры этого языка относительно компактны, особенно в сравнении с таким языком, как Аг(а.
Но его возможность расширять типы данных обеспечивает ему большую мощь в случае написания сложных программ. МЬ включает создание и обработку исключительных ситуации (исключений), императивное и функциональное программирование, основанные па правилах спецификации, и большую часть концепций, представленных в других языках программирования. Если бы потребовалось выбрать один-единственный язык для изучения многих концепций языков программирования, то МЕ оказался бы наиболее подходящим кандидатом, пока не встал бы вопрос о коммерческой живучести. МЬ завоевал большую популярность в исследовательских кругах и в области компьютерного образования. Доступность механизма определения типов данных на уровне исходной программы — то свойство М(., которое выгодно отличает его от других распространенных языков программирования. Однако коммерческих приложений, написанных на языке М(., практически нет; до сих пор он остается всего лишь инструментом при проведении теоретических исследований в области информатики и широко используется в образовании.
М1 был разработан группой программистов во главе с Робертом Милнером (КоЬегг Мйпег). Этот язык был задуман как механизм для построения (при помощи компьютера) формальных доказательств в системе логики для вычислимых функций, разработанной в середине 70-х гг в Эдинбурге (ЕсйпЬпгйЬ Еой)с (ог Соп1рпгаЫе Рнпссгопз). Но оказалось, что МЬ также полезен и в области символьных вычислений. В 1983 г. язык был пересмотрен, дополнен такими концепциями, как модули, н стал называться «стандартный М(.» (8сапдагд М1 ). Хотя обычно оп реализуется как интерпретируемый язык, сравнительно легко можно создать и использовать его компилируемую версию.
Первые компиляторы МЕ появились в 1984 г. (251 4.2. Семантика языка 169 К концу 80-х гг. Ягап|!аг|! М1. уже распространился в среде исслелователей языков программирования. Одна из популярных версий М1. была разработана Дэвидом Аппелем (РачЫ Арре!) из Принстонского университета и Дэвидом Маккуином (Раи|! МасОнееп) из АТе Т Вей Те1ер!юпе 1аЬогагог1ез.
Именно эта версия использовалась для проверки примеров программ на М1., которые приведены в нашей книге. Краткий обзор языка. М). — это сильно типизированный язык со статическим контролем типов и аппликативным выполнением программ. Отличие его от других представленных в этой книге языков заключается в том, что программист не должен объявлять типы данных — для этого существует специальный механизм вывода типа данных результирующих выражений. Этот механизм вывода типов делает возможным перегрузку и сопоставление с образцом на основе унификапии, почти как в языке Рго!ой. Как и в языке 1.!ЯР, программа на М 1. состоит из определений нескольких фун кцнй.
Каждая функция имеет статически определяемый тип и может возвращать значения любого типа. Поскольку М(.является аппликативным языком, то хранение переменных в нем осуществляется иначе, чем в языках С или РОВТ(сАЬ!. В М1. имеешься только ограниченная форма присваивания. Функциональное выполнение программы на М1. подразумевает, что параметры функций передаются по значеншо с созданием новой копии любого сложного объекта, используя кучу.
Комментарии в М1 обозначаются следующим образом; ('...*). В отличие от многих других языков в М1. комментарии могут быть вложенными. Как уже говорилось, в М1. реализовано большинство свойств языков программирования, которые мы рассматриваем в этой книге. Он позволяет создавать записи и абстрактные типы данных, а также создавать и обрабатывать исключения. Возможности ввода- вывода в М1. не очень велики, что обусловлено областью его применения — большинству исследователей пе требуется обрабатывать многочисленные базы данных с использованием сложных форматов. Синтаксис это|о языка достаточно лаконичен по сравнению с синтаксисом С++ или Аг!а. 4.2.4.
Проверка правильности программы ?1рн разработке и написании программ все большее значение придается их корректности и надежности. Современные языки имеют в своем арсенале инструменты для улучшения этих характеристик создаваемых программ. Некоторые концепции, упоминавшиеся нами при обсуждении семантики языка, могут помочь найти ответы на три вопроса, имеющих отношение к корректности программы.
!. Дана программа Р, каков ее смысл? Иными словами, какова спецификация В этой программы? 2. Дана спецификация 8, как разработать программу Р, которая реализует эту спецификацию? 3. Выполняют ли одну и ту же функцию программа 1' и ее спецификация В? Первый из этих вопросов непосредственно связан с моделированием семантики языка программирования, рассмотренным в разделе 4.2.2.
Второй вопрос сводится к задаче построения хорошей программы по заданной спецификации (на 170 Глава4. Моделирование свойств языка Прввило Следствие Предпооылкв (Р)5(Р) (Р)5(0) (Р)5, 5~(Р) (Р)5(О). (О ы Р) Я => Р). (Р)5(0) (Р)5;(О). (0)5к(а) К Консеквенция, 2. Консекввнцияк 3. Композиция сегодняшний день это центральная задача в технологиях разработки программного обеспечения). Третий вопрос формулирует основную проблему проверки правильности программы, то есть соответствия программы ее спецификации. Хотя эти три вопроса различаются по форме, они одинаковы по существу.
Третья формулировка была популярна в 70-е гг,, первая — с середины 70-х до конца 80-х, а вторая представляет большой интерес для современных исследователей. Однако ответы на все три вопроса следует искать с помощью схожих методов. Тестирование программы не может гарантировать отсутствие ошибок, за исключением лишь очень простых программ, При тестировании программа выполняется несколько раз, причем для каждого раза входные данные берутся из специального тестового набора Результат выполнения программы сравнивается с входными данными. Если результаты достаточно большой серии проверок неизменно оказываются правильными, то программа называется отлаженной.
Но на самом деле мы знаем только то, что программа корректно работает с тестовыми входными данными. В других случаях программа может ошибаться, Но перебрать все допустимые входные данные, как правило, невозможно. Таким образом, при проверке программ мы должны удовлетвориться неполной гарантией ее корректности. Если бы существовал какой-либо метод проверки правильности программы, не основанный на тестировании, то программы стали бы более надежными. Программа всегда вычисляет какую-нибудь функцию.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
