Как сделать включение схемы в другую схему с использованием языка Z

Question

Я пишу формальную спецификацию для моей модели, используя z-нотацию Z-языка. Я застрял и не знаю, как включить одну схему в другую схему и создает ее переменные в других схемах. Любое руководство и помощь будут оценены. Благодарю.

Answer 1

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

--- Complex ---
| real, img: ℤ
------

Вы можете объявить переменную в другой схеме такого типа:

--- Ex1 ---
| c: Complex
----
| c.real = 5 ∧ c.img = 6
-------

Конечно, вы можете создать более сложные типы данных с помощью последовательности и операции для добавления элемента:

--- State ---
| data: seq Complex
-------

--- Add1 ---
| ΔState
| real?, img?: ℤ
----
| ∃ c:Complex · c.real = real? ∧ c.img = img? ∧ data' = data^<c>
-------

Вы также можете использовать тэта-оператор для создания экземпляра этого типа. Значения для переменных взяты из текущего контекста (+ необязательные декорации):

--- Add2 ---
| ΔState
| real?, img?: ℤ
----
| data' = data^< θComplex? >
-------

θComplex? это пример Complex где значения для real а также img взяты из локальных переменных real? а также img?,

Мы также можем объявить входные переменные, используя исходную схему, и написать операцию более кратко (Add3 такой же, как Add2):

--- Add3 ---
| ΔState
| Complex?
----
| data' = data^< θComplex? >
-------

(Я удалил свой первоначальный ответ, потому что я неверно истолковал ваш вопрос.)

Answer 2

Как это

--- Agent---
| state: AgentState
-------

--- Shape ---
| agents :F Agent
----
| ∃ agt:agents · agt.state = stationary                                                         
 -------