Языки и методы формальной спецификации (1158803), страница 5

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

id : type_expr₁  …  type_expr_n opt-access_desc-string type_expr_n+1

id(binding₁,…,binding_n) post_condition opt-pre_condition

где n  1, является краткой формой следующих определений:

value

id : type_expr₁  …  type_expr_n opt-access_desc-string type_expr_n+1

axiom

 binding₁ : maximal(type_expr₁),…, binding_n : maximal(type_expr_n) •

id(express(binding₁),…,express(binding_n)) post_condition opt‑pre_condition

Если список связываний binding₁,…,binding_n пуст, то выражение type_expr₁  …  type_expr_n должно быть Unit и использовать квантор не нужно.

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

Аналогичное расширение имеет место, когда в качестве функциональной стрелки используется символ .

Подобным же образом рассматривается случай, когда конструкция id_application содержит более одного формального параметра formal_function_parameter.

Если в качестве значения метапеременной formal_function_application используется prefix_application, то неявное определение функции implicit_function_def вида:

value

prefix_op : type_expr₁ opt-access_desc-string type_expr₂

prefix_op id post_condition opt-pre_condition

является краткой формой определений:

value

prefix_op : type_expr₁ opt-access_desc-string type_expr₂

axiom

 id : maximal(type_expr₁) •

prefix_op id post_condition opt-pre_condition

В данном случае диапазон значений формального параметра id шире максимального типа соответствующего формального параметра type_expr₁.

Аналогичное расширение имеет место для функциональной стрелки .

Если в качестве значения метапеременной formal_function_application используется infix_application, то неявное определение функции implicit_function_def вида:

value

infix_op : type_expr₁  type_expr₂ opt-access_desc-string type_expr₃

id₁ infix_op id₂ post_condition opt-pre_condition

является краткой формой для определений:

value

infix_op : type_expr₁  type_expr₂ opt-access_desc-string type_expr₃

axiom

 id₁ : maximal(type_expr₁),id₂ : maximal(type_expr₂)•

id₁ infix_op id₂ post_condition opt-pre_condition

Здесь каждый формальный параметр id_i диапазоном своих значений превосходит максимальный тип соответствующего формального параметра type_expr_i.

Аналогичное расширение справедливо для функциональной стрелки .

3.5. Объявление переменных (Variable Declarations)

Синтаксис:

variable_decl ::=

variable variable_def-list

variable_def ::=

single_variable_def │

multiple_variable_def

single_variable_def ::=

opt-comment-string id : type_expr opt-initialisation

initialisation ::=

:= pure-value_expr

multiple_variable_def ::=

opt-comment-string id-list2 : type_expr

Терминология. Переменная – это некая сущность, в которой могут храниться значения некоторого типа. Присваивание значения переменной означает запоминание этого значения в указанной переменной. Значение может быть присвоено переменной явно с помощью выражения присваивания (см. раздел 6.20).

Под состоянием спецификации понимается присваивание значений всем переменным, определенным в объектах данной спецификации.

Определение переменной single_variable_def является циклическим, если максимальный тип выражения type_expr зависит от переменной, которая сама задается этим определением single_variable_def.

Максимальный тип зависит от переменной v , если он ссылается на v или на любую другую переменную или канал, чей максимальный тип зависит от v.

Контекстно-независимые расширения. Множественное определение переменных multiple_variable_def есть краткая запись двух или более определений каждой отдельной переменной, т.е. определение переменных multiple_variable_def вида:

variable id₁, … ,id_n : type_expr

является краткой формой для определений:

variable

id₁ : type_expr,







id_n : type_expr

Контекстные условия. Все входящие в объявление переменных variable_decl определения переменных variable_def должны быть совместимы.

Определение переменной single_variable_def не должно быть циклическим.

В инициализации initialisation выражение value_expr должно представлять собой чистое выражение, и его максимальный тип должен быть меньше или равен максимальному типу определяемой переменной.

Атрибуты. В определении переменной single_variable_def максимальным типом соответствующего id является максимальный тип выражения type_expr.

Максимальное определение для определения переменной single_variable_def получается путем замены входящего в это определение типового выражения type_expr на соответствующее выражение для максимального типа и удаления инициализации (если она присутствует).

Семантика. Определение переменной single_variable_def задает конкретный идентификатор id для некоторой переменной, в которой могут храниться значения максимального типа для типа, представленного выражением type_expr. Типом этой переменной является тип, представленный выражением type_expr.

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

Если инициализация initialisation не задана, начальным значением переменной считается некоторое произвольным образом выбранное значение внутри ее типа.

3.6. Объявление каналов (Channel Declarations)

Синтаксис:

channel_decl ::=

channel channel_def-list

channel_def ::=

single_channel_def │

multiple_channel_def

single_channel_def ::=

opt-comment-string id : type_expr

multiple_channel_def ::=

opt-comment-string id-list2 : type_expr

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

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

Определение канала single_channel_def является циклическим, если максимальный тип выражения type_expr зависит от канала, который сам задается тем же определением single_channel_def.

Максимальный тип зависит от канала c , если он ссылается на c или на любой другой канал или переменную, максимальный тип которой зависит от c.

Контекстно-независимые расширения. Множественное определение multiple_channel_def является сокращенной формой для двух или более определений каждого отдельного канала, т.е. определение каналов multiple_variable_def вида:

channel id₁, … ,id_n : type_expr

является краткой формой для определений:

channel

id₁ : type_expr,







id_n : type_expr

Контекстные условия. Все входящие в объявление каналов channel_decl определения каналов channel_def должны быть совместимы.

Определение канала single_channel_def не должно быть циклическим.

Атрибуты. В определении канала single_channel_def максимальным типом соответствующего id является максимальный тип выражения type_expr.

Максимальное определение для определения канала single_channel_def получается путем замены входящего в это определение типового выражения type_expr на соответствующее выражение для максимального типа.

Семантика. Определение канала single_channel_def задает конкретный идентификатор id для некоторого канала, по которому могут передаваться значения, тип которых представлен выражением type_expr.

3.7. Объявление аксиом (Axiom Declarations)

Синтаксис:

axiom_decl ::=

axiom opt-axiom_quantification axiom_def-list

axiom_quantification ::=

forall typing-list •

axiom_def ::=

opt-comment-string opt-axiom_naming readonly_logical-value_expr

axiom_naming ::=

[ id ]

Контекстно-независимые расширения. Любое объявление аксиом axiom_decl может быть расширено до объявления следующего вида:

axiom

opt-axiom_naming₁ □ value_expr₁,







opt-axiom_naming_n □ value_expr_n

В случае отсутствия конструкции axiom_quantification объявление аксиом axiom_decl вида:

axiom

opt-axiom_naming₁ value_expr₁,







opt-axiom_naming_n value_expr_n

является краткой формой объявления:

axiom

opt-axiom_naming₁ □ value_expr₁,







opt-axiom_naming_n □ value_expr_n

Конструкция axiom_quantification является сокращенной записью для дистрибутивной квантификации, т.е. объявление axiom_decl вида:

axiom forall typing-list •

opt-axiom_naming₁ value_expr₁,







opt-axiom_naming_n value_expr_n

представляет собой краткую форму записи объявления:

axiom

opt-axiom_naming₁ □  typing-list • value_expr₁,







opt-axiom_naming_n □  typing-list • value_expr_n

Контекстные условия. Все входящие в объявление аксиом axiom_decl определения axiom_def должны быть совместимы.

Входящее в определение аксиомы axiom_def выражение value_expr должно быть доступно только для чтения (read-only), и его максимальный тип должен быть Bool.

Семантика. Определение axiom_def устанавливает в терминах некоторой аксиомы (в виде соответствующего булевского выражения value_expr) свойства сущностей, заданных где-то в другом месте спецификации.

Аксиома может быть снабжена именем (id в конструкции axiom_naming).

1. Описание классов (Class Expressions)

4.1. Общие положения

Синтаксис:

class_expr ::=

basic_class_expr │

extending_class_expr │

hiding_class_expr │

renaming_class_expr │

scheme_instantiation

Терминология. Модель представляет собой некоторую ассоциацию идентификаторов и операций с какими-либо сущностями. Модель обеспечивает какой-либо идентификатор или операцию, если она ассоциирует этот идентификатор или операцию с некоторой сущностью.

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

Класс представляет собой набор моделей.

Идентификатор или операция является недоспецифицированным (under‑specified), если в классе существует по крайней мере две модели, в которых данный идентификатор или операция ассоциируется с различными сущностями.

Класс class_expr₁ является подклассом класса class_expr₂, если все модели класса class_expr₁ являются моделями класса class_expr₂.

Характеристики

Список файлов книги