Калайда В.Т., Романенко В.В. Технология разработки программного обеспечения (2007), страница 11

Однако имеется одно существенное различие между переменнымитипа FIXED и BLIPPO. Переменная типа FIXED размещается впамяти, когда начинает выполняться процедура (или блок), содержащая объявление переменной, и освобождает память, когдапроцедура (блок) завершится. А для переменной типа BLIPPO73должна быть выделена постоянная память.

Это может привестик двусмысленной ситуации. Так как одна из целей примененияданных абстрактного типа заключается в расширении типовданных для прикладных задач, различие между типами данных,генерируемых компилятором, и данных, созданных пользователями, может вызвать недоразумения. Следовательно, одной иззадач проектирования с использованием данных абстрактноготипа должно быть автоматическое размещение таких данныхпри их использовании, так чтобы не было различий в стратегиииспользования памяти для указанных двух типов данных.Для того чтобы использовать автоматическое распределение памяти, переменная Х инициируется при вызове модуляSTACK. По существу, компилирование объявления ENVIRONMENT эквивалентно следующей записи.declare X POINTER INITIAL(STACK);При первоначальном обращении к модулю STACK распределяется память для стека Х и возвращается ее адрес в переменную-указатель.

Модуль, в котором происходит обработкастека Х, имеет вид:STACK: ABSTRACTION;REP 1 STACK[X], /* имя параметра стека*/2 ENTRIES(100) FIXED,2 TOPOFSTACK FIXED;/* разместить стек *//* присвоить начальные значения */TOPOFSTACK = 0;PUSH: function(X, элемент);...end;POP:function(X, элемент);...74end;...end;Такую процедуру легко написать на современных языках,учитывая следующее.Начало процедуры ABSTRACTION предназначено дляразмещения данных абстрактного типа и присвоения им начальных значений; однако действительным распределением памятиавтоматически занимается компилятор.

Это делается для сохранения совместимости с элементарными типами данных, такими,как FIXED и REAL.Слово ABSTRACTION заменяется ключевым словомPROCEDURE и добавляется атрибут RETURN(POINTER). Кроме того, используются следующие операторы:declare DUMMY POINTER;ALLOCATE datatype SET(DUMMY);Эти операторы позволяют автоматически распределятьпамять для данных абстрактного типа.

Для того чтобы обеспечить возврат из подпрограммы распределения памяти к соответствующему оператору declare, перед первым операторомFUNCTION помещают оператор RETURN(DUMMY). Вместо оператора REP объявляется структура типа BASED. Таким образом,транслятор транслирует следующие операторы:STACK: procedure RETURNS(POINTER);declare 1 STACK BASED(X),2 ENTRIES(100) FIXED,2 TOPOFSTACK FIXED;declare DUMMY POINTER;ALLOCATE STACK SET(DUMMY);TOPOFSTACK = 0;return(DUMMY);end;75Вместо оператора FUNCTION подставляется последовательность ENTRY BEGIN. Для соответствующих операторовEND добавляются операторы RETURN.

Таким образом, имеем:STACK: procedure RETURNS(POINTER);declare 1 STACK BASED(X),2 ENTRIES(100) FIXED,2 TOPOFSTACK FIXED;declare DUMMY POINTER;ALLOCATE STACK SET(DUMMY);TOPOFSTACK = 0;return(DUMMY)PUSH: function(X, элемент);...return;end;POP:function(X, элемент);...return;end;...end;Доступ к данным. При указанном способе организацииданных защитные меры приняты лишь отчасти: модуль не может получить представление любой переменной абстрактноготипа, определенное в некотором другом модуле. Однако долженли вообще данный модуль иметь доступ к определенным данным абстрактного типа? Окончательная версия программы имеет следующую структуру:Модуль176Модуль2…МодульnПри такой структуре программы каждый модуль можетпользоваться любой функцией любого другого модуля. Однакоэто может оказаться нежелательным. Предположим, что модульX использует абстрактный тип данных Y, который, в свою очередь, обращается к абстрактному типу данных Z (рис.

4.14).XYZХ известно о Y;Y известно о Z;Х неизвестно о ZаXYZХ вызывает Z непосредственнобРис. 4.14 — Нарушение принципа информационной локализованностиПри написании программы программист, стремясь кбольшей эффективности программы, записывает вызов из модуля Х данных Z, тем самым неумышленно нарушает спецификацию относительно того, что о структуре данных Z известнотолько в модуле Y. Однако компилятор не в состоянии проверить это нарушение, а ошибка может быть выявлена гораздопозже, например, если модуль Y когда-либо изменится.В операционных системах имеется возможность защитыот некорректных действий; такую форму защиты можно добавить в языки программирования. В операционных системахимеется вектор возможностей, связанный с каждым независимо выполняемым процессом.

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

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

Язык проектирования программ PDL. Операторы выбора. Операторы цикла. Операторы описания данных.Операторы ввода/вывода и вызова процедур. Операторleave. Предложения на естественном языке.2. Нисходящее проектирование и нисходящая разработка.3. Пошаговое совершенствование.4. Восходящее проектирование.5. Подыгрывающие программы (заглушки).6. Структурное проектирование. Простая программа.Элементарная программа. Управляющие структуры,способы их описания.7. Скалярные и агрегативные типы данных.8. Массивы.

Структуры. Списки. Очереди. Стеки. Множества. Графы. Деревья.9. Абстрактные конструкции.10. Фиксированные данные абстрактного типа.11. Размещение указателей.12. Защита данных от несанкционированного доступа.785 ПРАВИЛЬНОСТЬ ПРОГРАММОдним из важных методов повышения эффективностипроектирования программ является верификация программ илиматематическое доказательство того, что программа работаетправильно. Для доказательства правильности программ используется аксиоматический подход, при котором применяется теория перечисления предикатов.

Предполагается, что каждый оператор в программе выполняет заранее определенные действия,зависящие только от синтаксиса языка. Для двух предикатов Pи Q и оператора S необходимо определить, истинно ли выражение:«Если P истинно и если выполняется оператор S, то Q истинно».Предикат P является спецификацией правильного выполнения оператора S, а предикат Q будет истинным после выполнения оператора S и является спецификацией следующего за Sоператора.Если это утверждение распространить на все операторыпрограммы и если P является спецификацией первого оператора, а Q истинно после окончания программы, то будет доказанаправильность всей программы относительно предикатов P и Q.Эту конструкцию можно записать в следующем виде:{ P} S { Q} ,где P называется предусловием истинности Q после выполнения программы S.Доказательство правильности программы заключается вопределении, является ли выражение {P}S{Q} истинным относительно входных спецификаций P, выходных спецификаций Q иоператоров S программы.

Если {P}S{Q} истинно, то это означает,что доказана правильность программы S относительно P и Q.5.1 АксиомыДля целей доказательства правильности программ к правилам исчисления предикатов следует добавить правила, необходимые для выполнения последовательности операторов программы. Эти правила, называемые правилами следствия, формулируются следующим образом:791) если {P}S{Q} и Q  R, то {P}S{R};2) если {Q}S{R} и P  Q, то {P}S{R}.Первое правило заключается в следующем: «Если P —предусловие для Q и если Q  R является теоремой исчисленияпредикатов, то P — предусловие для R». Таким образом, если Pистинно и выполняется S, то R (так же, как и Q) истинно.Второе правило следствия аналогично данному. Эти правила следствия можно представить в более формальном виде:числитель выражения является посылкой, а знаменатель — заключением:1)2){ P} S { Q} , Q{ P} S { R}{ Q} S { R} , P{ P} S { R}RQ;.Правила следствия используются для доказательствасложных элементов программы.

Пусть программа представленав виде структуры (рис. 5.1), где Si — операторы, а Pi — предикаты, соответствующие дугам.S1НачалоP1S2P2КонецP3Рис. 5.1 — Структура программыПредположим, что доказаны следующие утверждения:{P1}S1{P1'} и {P2}S2{P2'} для некоторых предикатов P1' и P2'.Если можно доказать, что P1'  P2 и P2'  P3, то, используяправила следствия, можно доказать, что {P1}S1;S2{P3} истинно.Следует определить, какие операторы программы являются правильными. Предполагается, что программа состоит только из последовательности операторов присвоения и операторовif и do while.Так как только оператор присвоения может изменять значение переменных, то для определения правильности оператораприсвоения нужно добавить только одну аксиому, она называ-80ется аксиомой присвоения и формулируется следующим образом:x = expr, P ( x ){ P ( expr ) } x = expr { P ( x ) }.В соответствии с этой аксиомой устанавливается, чтоесли P — утверждение, содержащее переменную x, истинно, тоP должно быть истинно и до выполнения оператора присвоения, если x изменяется expr.Например, если P(x) является предикатом x > 0 и x = x + 1— оператор присвоения, то P(x + 1) является предикатомx + 1 > 0 или x > –1.По правилам следствия, если можно доказать, что Q P(x + 1) для некоторого предиката Q, то справедливо утверждение {Q}x = x + 1{x > 0} и предикат является предусловием для P.Осталось определить правильные управляющие структуры.

Введем следующие аксиомы.Аксиома следования:{ P} S1 { Q} ,{ Q} S2 { R} .{ P} S1; S2 { R}Два оператора программы могут быть объединены. Еслипосле выполнения S1 предикат Q остается истинным и Q естьпредусловие для оператора S2, то P является предусловием дляоператоров S1; S2.Аксиома цикла:{ P & B} S { P}{ P} do while ( B ) ; and ;{B & P}.Утверждается, что если истинность P не изменяется оператором S (т.е. является инвариантом), то P инвариантно относительно цикла, содержащего S.