Конспект установочных лекций по комплексному курсу Информатика, Теория информации


Формализмы для спецификаций - часть 4


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

Спецификация функций

Одной из самых элементарных концепций математики являются функции и абстракции функций. Программы (вычислительные предписания) в простейшем случае реализуют (вычисляют) определенные функции. Тем самым спецификация программ соответствует спецификации функций.

Чтобы специфицировать функцию 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.

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

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

 

Спецификация операторов

Оператор представляет собой функцию (или - в недетерминированном случае - отношение) между состояниями. Состояния можно понимать как специальный объект некоторого типа.


- Начало -  - Назад -  - Вперед -



Книжный магазин