1

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.

Yasir Darr
  • 43
  • 6

2 Answers2

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.)

danielp
  • 1,179
  • 11
  • 26
  • danielp , you guided me in a right direction. Now the only thing which is still confusing me. how can we declare this variable as a collection of that schema? That is, can we use Fat F to represent a finite collection of that schema. – Yasir Darr Dec 06 '17 at 13:25
  • 1
    @YasirDarr: Yes, you can declare it exactly like the sequence above, just use Complex instead of seq Complex. Like you did in your additional answer. – danielp Dec 06 '17 at 15:38
  • Alright dear, Now it seems that I will be able to solve my issue. (y) – Yasir Darr Dec 06 '17 at 16:35
0

Like this

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

--- Shape ---
| agents :F Agent
----
| ∃ agt:agents · agt.state = stationary                                                         
 -------
Yasir Darr
  • 43
  • 6