Нотация Z: как написать схему операции, которая может добавить один или несколько кортежей к отношению

Я пишу схему операции в Z. Эта операция AssignValue сопоставляет свойство с одним или несколькими значениями.

Одно свойство может быть связано с одним или несколькими значениями, а одно значение может быть связано с одним или несколькими свойствами, образуя отношение «многие ко многим» R ⊆ свойство × значение.

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

Версия А:

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

В версии B я добавил powerset в объявление v? указать, что v? представляет собой набор значений (более одного значения).

Версия Б:

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

Какая версия правильная? или есть лучший способ представить это? Я новичок в z-нотации, буду признателен за любую помощь. Спасибо!


formal-languages formal-methods z-notation
person snow    schedule 01.07.2019    source источник

Ответы (2)


arrow_upward
0
arrow_downward

Вы не показали всей схемы. Я предполагаю, что у вас есть схема состояния S с отношением R : Property<->Value (эквивалентным R ⊆ Property × Value), а AssignValue включает ∆S.

Оба стиля могут работать, хотя ваша версия B, вероятно, не соответствует вашим намерениям.

Отношение может иметь много пар с одним и тем же элементом предметной области, поэтому начиная с

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

Вы можете вызвать AssignValueA с помощью p?=p0, v?=v16, чтобы получить состояние с помощью

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

то есть p0 теперь отображается на три отдельных значения.

В вашей версии B у вас есть то же самое, но теперь ваши значения представляют собой наборы значений. Вероятно, вы имели в виду, что R будет суммарной функцией типа Property → Value. Теперь, предполагая только свойства с p0 по p3, у вас будет начальный R как

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

Вам нужно определить

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

Он имеет тот же интерфейс, что и AssignValueA, позволяя добавлять одно значение к одному свойству за вызов.

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

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

person user1513683    schedule 16.08.2019

arrow_upward
0
arrow_downward

В качестве примера большой спецификации Z я предлагаю этот недавно загруженный проект: https://github.com/vinahradau/finma

Для «один ко многим» я бы использовал отношение (в отличие от функции).

Пример из проекта выше:

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