|
message, data -> message, data ->• message, message, data -> message, message, |
put_empty:
padd:
pdelete:
sisempty:
siselem:
sany:
|
data bool |
Output Channel Messages:
|
message, message, |
data:
bool:
Axioms:
(см. табл.11.1) end_of_class
Поведение объекта класса задано таблицей переходов состояний. Здесь речь идет о примере класса 00-языка программирования с параллельной моделью
выполнения.
Таблица 11.1. Таблица переходов состояний для класса
|
Ввод |
Состояние ввода |
Вывод |
Следующее состояние |
|
Putempty |
S |
Empty |
|
|
Padd(d) |
S |
add(s, d) |
|
|
Pdelcte(d) |
S |
delete(s, d) |
|
|
Sisempty |
S |
bool(isempty(s)) |
S |
|
Siselem(d) |
S |
bool(iselem(s)) |
S |
|
Sany |
S |
data(any(s)) |
S |
Объекты возникают во время выполнения программы как воплощения классов. Во многих 00-языках программирования существуют универсальные методы специально для создания объектов. Созданные объекты, как правило, идентифицируются ссылками. В более сложных примерах также и ссылки на объекты могут возвращаться в качестве результатов.
Формализация этого обращения с классами и объектами возможна с помощью явного представления ссылок и создания объектов. Это ведет к понятию состояния по аналогии с состоянием памяти
Пример (классы с созданием объектов). Приведем типичный пример класса с созданием объекта:
class QUEUE_CLASS = Based on: QUEUE
Attributes: d : data, b : bool, s : Pointer to QUEUE_CLASS,
Methods: put_empty,
padd param data, pdeq
Selectors: qisempty: -> bool, qnext: -»data
Axioms: put_empty = [b := true ],
padd(x) = [if b then d := x;
b := false;
create(s);
s.put_empty(s) else s.padd(x) fi], pdeq = [if qisempty(s) then b :== true
else d :== qnext(s); s.pdeq(s) fi], qisempty = b, qnext = d
end_of_class
Концепция наследования касается таких составных частей класса, как: