type Collection

value

empty : Collection,

add : Elem ><Collection -> Collection

axiom

[ disjoint ]

all el : Elem, с : Collection :- empty ~= add(el,c),

[ induction ]

all p : Collection -> Bool :-

(p(empty) /\ (all el : Elem, с : Collection :- p(c) => p (add(el,c)))) =>

(all с : Collection :- p(c))

Деструкторы

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

В качестве примера рассмотрим вариантное определение:

type List = = empty | add(head : Elem, tail : List),

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

Данное вариантное определение является сокращением следующего фрагмента спецификации:

type List

value

empty : List,

add : Elem >< List -> List,

head : List -~-> Elem,

tail : List -~-> List

axiom

[ disjoint ]

all el : Elem, ls : List :- empty ~= add(el,ls),

[ induction ]

all p : List -> Bool :-

(p(empty) /\ (all el : Elem, ls : List :- p(ls) => p (add(el,ls)))) =>

(all ls : List :- p(ls))

[ head_add ]

all el : Elem, ls : List :- head(add(el,ls)) is el,

[ tail_add ]

all el : Elem, ls : List :- tail(add(el,ls)) is ls

Следует обратить внимание на частичность деструкторов head и tail, поскольку согласно исходному вариантному определению они определены только над значениями, сгенерированными конструктором add.

Реконструкторы

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

В качестве примера рассмотрим предыдущее определение типа List с добавлением реконструктора replace_head для обеспечения возможности изменения головы списка.

type List = = empty | add(head : Elem <-> replace_head, tail : List)

Вхождение реконструктора добавит к вышеприведенной спецификации следующий фрагмент:

value

replace_head : Elem >< List -~-> List

axiom

[ head_ replace_head ]

all el,el1 : Elem, ls : List :- head(replace_head(el,add(el1,ls))) is el,

/* изменилось значение головы списка */

[ tail_ replace_head ]

all el : Elem, ls : List :- tail(replace_head(el,ls)) is tail(ls)

pre ls ~= empty

/* реконструктор replace_head не меняет хвост списка */

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

Упражнения

1. Cчитая определенными абстрактные типы Key и Data, построить вариантное определение записи с полями «ключ» и «значение». Привести эквивалентное определение без использования вариантных определений.

Указания: используйте конструктор записей и деструкторы для декомпозиции записи на значения ее полей.

1. Cчитая определенным абстрактный тип Elem, построить вариантное определение стека. Привести эквивалентное определение без использования вариантных определений.

Указания: воспользуйтесь рекурсивным определением стека.

1. Для следующих вариантных определений привести эквивалентные определения без использования вариантных определений.

1. type Elem,

Collection = = empty | add1(Elem, Collection) |

add2(Elem, Elem, Collection)

1. type Elem,

Tree = = empty | node(left : Tree, val : Elem, rigth : Tree)

1. type Elem,

Tree = = empty | node(left : Tree, val : Elem <-> repl_val, rigth : Tree)

1. type Figure = = box(length : Real, width : Real) | circle(radius : Real) |

triangle(base_line : Real, left_angle : Real, right_angle : Real)

ГЛАВА 8. ИМПЕРАТИВНЫЙ СТИЛЬ СПЕЦИФИКАЦИЙ

Понятие императивного стиля спецификаций. Описание переменных. Выражение присваивания. Функции с доступом к переменным. Императивные конструкции RSL. Описание локальных переменных. Явные и неявные спецификации в императивном стиле. Упражнения.

Понятие императивного стиля спецификаций

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

Характерной особенностью императивного стиля является использование переменных как способа передачи информации от одного шага выполнения алгоритма к другому. В RSL переменная рассматривается как контейнер, способный хранить значения определенного типа. Значение переменной может быть изменено путем присваивания ей нового значения. Совокупность значений всех объявленных в данной спецификации переменных формирует понятие состояния спецификации.

Описание переменных

Описание переменных в языке RSL производится в разделе variable, при этом каждое отдельное описание переменной имеет вид:

id : type_expr := value_expr,

где id задает имя переменной, type_expr – ее тип, выражение value_expr определяет начальное значение переменной. Инициализация переменной ее начальным значением является необязательной, и если она не указана, начальным значением переменной считается произвольное значение данного типа. Однотипные переменные без начального значения могут объявляться в одном описании. Например:

variable n : Nat := 1,

s : Real = 0.0,

a, b : Int

Областью видимости переменной считается весь модуль, в котором данная переменная описана.

Выражение присваивания

Для изменения значения переменной в RSL используется выражение присваивания вида:

id := value_expr

В качестве побочного эффекта при вычислении такого выражения переменной id присваивается значение выражения value_expr, при этом само выражение присваивания возвращает значение () типа Unit. Типы переменной id и выражения value_expr должны быть согласованы, причем тип выражения value_expr не может быть типом Unit. Пример выражения присваивания:

counter := counter +1

Функции с доступом к переменным

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

write id₁, ..., id_n, n  1,

если функция имеет доступ к перечисленным переменным на запись (и чтение), или в форме:

read id₁, ..., id_n, n  1,

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

В качестве примера рассмотрим следующий фрагмент спецификации:

variable n, m : Nat

value

f1 : Unit -> write n Nat,

f2 : Unit -> read m Nat,

f3 : Nat -> write n read m Nat

Здесь функции f1 и f2 не имеют входных параметров и, следовательно, зависят только от конкретного состояния, в котором происходит их вычисление. При этом f1 имеет доступ к переменной n на чтение и запись, f2 – к переменной m только на чтение. Функция f3 имеет доступ к переменной n на чтение и запись и к переменной m только на чтение.

Императивные конструкции RSL

Последовательность выражений

Последовательная композиция двух выражений задается выражением вида:

value_expr₁ ; value_expr₂

Вычисление такого выражения начинается с вычисления выражения value_expr₁ с целью достижения его возможного побочного эффекта в виде изменения значений входящих в него переменных. Затем уже в измененном состоянии вычисляется выражение value_expr₂. В качестве результата вычисления последовательной композиции выражений возвращается значение выражения value_expr₂. Выражение value_expr₁ должно иметь тип Unit. Например:

x := 1; x - выражение возвращает значение 1,

x := x + 1; x - выражение возвращает увеличенное на 1 значение переменной x.

В общем случае произвольная последовательность выражений задается выражением:

value_expr₁ ; ... ; value_expr_n , где n > 1.

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

Выражение if

Выражение if в императивных спецификациях имеет традиционную форму:

if value_expr then value_expr₁ else value_expr₂ end,

спецификой является только то, что выражения value_expr₁ и value_expr₂ имеют тип Unit. Кроме того возможна сокращенная форма выражения в виде:

if value_expr then value_expr₁ end

Эта форма эквивалентна выражению:

if value_expr then value_expr₁ else skip end,

где skip представляет предопределенное выражение типа Unit, не имеющее побочного эффекта.

Например:

if counter > 0 then counter := counter - 1 end

Конструкции циклов

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

• цикл с предусловием (while),

• цикл с постусловием (until),

• цикл с заранее известным числом повторений (for).

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

Цикл while

Конструкция цикла while представлена выражением while вида:

while value_expr do value_expr₁ end,

где выражение value_expr (тип Bool) задает условие повторения цикла, выражение value_expr₁ (тип Unit) – тело цикла (обычно последовательность выражений). Вычисление выражения while состоит из выполнения последовательных итераций. Каждая итерация цикла начинается с вычисления условия value_expr, и в случае его истинности выполняется вычисление выражения value_expr₁, после чего итерация повторяется, в противном случае вычисление выражения while завершается.

Цикл until

Конструкция цикла until представлена выражением until вида:

do value_expr₁ until value_expr end

Назначение выражений value_expr и value_expr₁ аналогично их назначению в предыдущей конструкции с той лишь разницей, что value_expr обозначает условие завершения цикла и в случае истинности этого условия вычисление выражения until завершается.

Цикл for

Конструкция цикла for представлена выражением for вида:

for list_limitation do value_expr₁ end,

где list_limitation задает список (возможно пустой) значений переменной цикла. Тело цикла (выражение value_expr₁) последовательно вычисляется для всех значений из указанного списка. Например:

for i in <. 1 .. n .> do

result := result + 1.0 / (real i)

end

Описание локальных переменных

В императивных спецификациях часто бывает удобно использовать локальные переменные. Объявление локальной переменной имеет вид:

local