Z notation: How to write operation schema that may add one or more tuples to a relation

Question

I'm writing an operation schema in Z. This operation AssignValue maps a property to one or more values.

One property may be linked to one or more values, and one value may be linked to one or more properties, forming a many-to-many relation, R ⊆ Property × Value.

I'm not sure how to write this operation to indicate that one property could be mapped to one or more values. I have two versions here. Version A seems to map one property to only one value.

Version A:

--AssignValue---
| p? : Property
| v? : Value
-------
|R′ = R ∪ { p? ↦ v? }
-------

In Version B, I have added a powerset in the declaration of v? to indicate that v? is a set of values (more than one value).

Version B:

--AssignValue---
| p? : Property
| v? : P Value
-------
|R′ = R ∪ { p? ↦ v? }
-------

Which version is correct? or there is a better way to represent this? I'm new to z-notation, any help would be greatly appreciated. Thanks!

Answer 1

You have not shown the whole schema. I assume that you have a state schema S with a relation R : Property<->Value (equivalent to R ⊆ Property × Value) and AssignValue includes ∆S.

Both styles could work, although your version B is probably not what you intended.

A relation is allowed to have many pairs with the same domain element, so starting with

R = {p0 ↦ v0, p0 ↦ v1, p3 ↦ v16}

You could call AssignValueA with p?=p0, v?=v16 to get a state with

R = {p0 ↦ v0, p0 ↦ v1, p0 ↦ v16, p3 ↦ v16}

that is, p0 is now mapped to three separate values.

In your version B you have exactly the same thing, but your values are now sets of values. What you probably intended was that R would be a total function of type Property → Value. Now, assuming only properties p0 through p3, you would have the initial R as

R = {p0 ↦ {v0, v1}, p1 ↦ ∅, p2 ↦ ∅, p3 ↦ {v16}}

You need to define

--AssignValueB----------------
| ∆S
| p? : Property, v? Value
------------
| R' = R ⊕ {p? ↦ R p? ∪ {v?}}
------------------------------

This has the same interface as AssignValueA, allowing addition of a single value to a single property per call.

In both models a property may have no, one or many associated values, but the operation only allows one property to be assigned one extra value per call.

Exercise: try defining an operation that allows multiple properties to be assigned multiple extra values per call.

Answer 2

For an example of a big Z specification, I suggest this recently uploaded project: https://github.com/vinahradau/finma

For a one-to-many, I would use a relation (as an opposite to a function).

Example form the project above:

userAccessRigths: USER ↔ ROLE
userAccessRigths′ = userAccessRigths ∪ {(user?, role?)}