How to do inclusion of schema in other schema using Z language

Question

I am writing a formal specification for my model using z-notation of Z-language. I am stuck and don't know how to include one schema in another schema and creates its variables in other schemas. Any guidance and help would be appreciated. Thanks.

Answer 1

You can use a schema like a record data type. E.g. let's assume you have a schema describing a complex integer number:

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

You can declare a variable in another schema to be of that type:

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

You can of course create more complex data types with it, here a sequence and an operation to append an element:

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

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

You can also use the theta-operator to create an instance of that type. The values for the variables are taken from the current context (+ optional decorations):

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

θComplex? is an instance of Complex where the values for real and img are taken from the local variables real? and img?.

We can also declare the input variables by using the original schema and write the operation more concise (Add3 is the same as Add2):

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

(I deleted my original answer because I misinterpret your question.)

Answer 2

Like this

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

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