Конспект установочных лекций по комплексному курсу Информатика, Теория информации
Формализмы для спецификаций
Cуществует много различных стилей и формализмов для описания требований, данных и алгоритмов которые находят примеyение при проектировании, разработке и aнализе программных систем. Различные формализмы по-разному удовлетворяют общим требованиям к нотации, таким, как:
·
простота чтения и понимания,
· легкость овладения,
· мощность (границы возможностей нотации),
· выполнимость,
· эффективность выполнения.
Какие веса придать этим критериям, сильно зависит от специфики приложений. В данной главе дадим краткое введение в некоторые основные методы описания и программирования.
Для формулирования эффективных алгоритмов, безусловно, требуется точно установить, что должно быть вычислено, не вникая сначала в то, как (по какому алгоритму) это будет вычисляться. Мы говорим о спецификации задачи или о спецификации требований.
Абстракция в спецификации
В программировании оказывается полезным различать абстрактные вычислительные структуры
(называемые также абстрактными типами данных) и структуры данных.
При этом, точнее говоря, речь идет исключительно о разных взглядах на типы и на функции, имеющиеся для них в распоряжении.
Абстрактные структуры данных представляют вид доступа для типа s или для семейства типов. При этом устанавливается, какие основные операции имеются в распоряжении для элементов данных этого типа. Для этого в сигнатуре задаются доступные для использования функции и их функциональности. Относительно символов функций делается различие между
· селекторами для доступа к составным частям элемента данных,
· функциями опроса для установления определенных свойств данных
· (дискриминаторы),
· функциями-конструкторами для построения элементов данных.
В дальнейшем будет использоваться простой частный случай, когда задается вычислительная структура для описания структуры доступа только для одного типа s. Конечно, эти вычислительные структуры опираются на другие типы, которые предполагаются заданными. Функции-конструкторы в качестве типа результата принципиально имеют тип s. Если аргументы функции-конструктора также имеют тип s, то описываемый тип будем называть рекурсивным. При рекурсивных типах также и определенные функции-селекторы имеют тип результата s.
Если в связи с типом s говорится о структуре данных, то тем самым имеется в виду внутреннее строение элементов данных типа s. Это определяет, каким образом структурируются элементы данных внутри себя и как конкретно они реализуются в памяти ЭВМ.
Различение аспектов реализации (англ. Glass Box View) и доступа (англ. Black Box View) является существенным для разработки программы. Аспект доступа определяет интерфейс (разрез) для типа или вычислительной структуры. Этого разреза достаточно для корректного использования типа и имеющихся для него операций. Для оценки эффективности нужны только данные о сложности по времени и по памяти используемых операций.
Аспект реализации касается лишь реализатора типа и содержит в себе все детали реализации. Аспект доступа представляет собой абстракцию аспекта реализации. Существует много структур данных для реализации одних и тех же абстрактных вычислительных структур. При использовании вычислительной структуры пользователю нужно знать лишь аспект доступа, реализация же может быть скрыта от него (англ. information hiding). Это имеет решающие преимущества:
· пользователь не обязан знать порой сложные, трудно просматриваемые детали реализации вычислительной структуры, ему достаточно знать лишь ее абстрактный аспект доступа. Этот аспект служит для документирования;
· реализация может производиться параллельно с программированием, при котором используется эта вычислительная структура.
Основой для взаимопонимания служит аспект доступа;
· реализация может быть изменена, и пользователь может даже не знать об этом, если только сохраняется аспект доступа.
Центральным для этого метода разделения аспектов доступа и реализации является понятие точки разреза, или интерфейса (англ. interface). Последовательное разделение этих аспектов является показателем хорошего стиля разработки программного оборудования, особенно при создании сложных программных систем. Этот принцип используется не только применительно к структурам данных - он может быть перенесен и на другие программные единицы, такие, как процедуры, модули и классы.
Для методов информатики особенно типично, что взгляды на типы как абстрактные структуры данных и как структуры данных разбиваются на слои. Здесь говорится об уровнях абстракции Так, над абстрактной вычислительной структурой Р, которая описывает платформу реализации, с помощью определенных функций можно построить аспект структуры данных для другой вычислительной структуры А. Здесь говорится о реализации одной из вычислительных структур .А над вычислительной структурой Р.
Спецификация абстрактных, вычислительных структур
При разработке программных систем одной из важнейших задач является выбор и спецификация основных вычислительных структур. Для описания вычислительных структур предлагаются следующие возможности:
· моделирование с помощью заданных структур (способ, ориентированный на модели), например через множества, отношения, абстрактные машины;
· характеризация свойств через логику предикатов или через законы равенств ("алгебраическая спецификация").
Ниже кратко обрисована техника алгебраических спецификаций, так как она особенно хорошо подходит для описания аспектов интерфейса. Вычислительную структуру можно алгебраически специфицировать путем
(1) задания сигнатуры,
(2) задания законов, характеризующих отображения.
Дадим несколько примеров алгебраических спецификаций. В алгебраической спецификации мы описываем абстрактную вычислительную структуру через ее сигнатуру и ее законы.
Спецификация функций
Одной из самых элементарных концепций математики являются функции и абстракции функций. Программы (вычислительные предписания) в простейшем случае реализуют (вычисляют) определенные функции. Тем самым спецификация программ соответствует спецификации функций.
Чтобы специфицировать функцию f, сначала задается ее функциональность. Например, пишется
Fct f= (s1,…..,sn) Sn+1.
Для заданной S -вычислительной структуры могут быть специфицированы с помощью равенств.
При этом задается некоторое количество правил, которые устанавливают требования к f, но не обязательно описывают функцию однозначно. В этом случае говорят, что функция f не полностью специфицирована.
Пример (спецификации функций). На вычислительной структуре BOX можно специфицировать, например, следующие функции.
(1) Увеличение на единицу всех элементов конечного множества:
дополнительно к функциональности
fct incr_all = (set nat) set nat,
задаются следующие два равенства:
incr_all(put(b, x)) = put(succ(b), incr_all(x)), incr_all(emptybox) = emptybox.
(2) Функция выбора для множества: дополнительно к функциональности
fct any = (set data s: not(isempty(s))) data задается следующее равенство:
iselem(put(b, x), any(put(b, x))) = true.
Наряду с равенствами для спецификации функций используются также общие предикаты. С помощью предикатов задаются, какие отношения существуют между входом и выходом.
Обращается внимание на то, что для многих постановок задач вовсе не обязательно, чтобы спецификация задавала функцию однозначно. Здесь говорится о степенях свободы в спецификации, о неполной спецификации или об открытости принятия решений по проекту.
Спецификация операторов
Оператор представляет собой функцию (или - в недетерминированном случае - отношение) между состояниями. Состояния можно понимать как специальный объект некоторого типа.
Представляются состояния как отображения множества программных переменных в VAR на значения из DATA. Тем самым для множества состояний STATE справедливо.
STATE = defVAR -> DATA.
Соответственно этому предикаты на состояниях можно представить в виде отображений вида
PRED: STATE -> В.
Эти предикаты могут использоваться в качестве утверждений для спецификации операторов. Оператор соответствует отображению
STATE -> STATE.
Метод утверждений позволяет специфицировать программу путем задания предикатов. Оператор специфицируется двумя предикатами, называемыми предусловием Q и постусловием R. При этом имеет место R, Q Î PRED. Оператор
f: STATE -> STATE
удовлетворяет этой спецификации, если справедливо следующее высказывание:
" s ÎSTATE: Q(s) => R(f(s)).
Таким образом, оператор специфицируется парой предикатов (Q, R). Утверждение Q может пониматься как предположение об исходном состоянии, а R специфицирует утверждение о выходном состоянии в случае выполнения предположения. Поэтому говорится также s спецификациях предположение/утверждение (англ. rely/guarantee или также assumption/commitment).
