問題タブ [z-notation]

完全な開示、これは大学のコース用です。私は完全な答えを期待していませんが、助けていただければ幸いです。

Z 表記を使用して Item エンティティをモデル化する必要があります。これは説明です：

アイテム: すべてのアイテムには、アイテムを一意に説明するために使用できる名前と一意の ID があります。アイテムには、価格 (正のフロート) とカテゴリもあります。

要件の一部は、量指定子なしでこれらのエンティティをモデル化することです。

これは私が最終的に得たものですが、それが正しいかどうかはわかりません:

アイテムのスキーマ

名前は文字列の組み合わせであり、ID は正の整数とその名前のタプルであり、価格とカテゴリの両方が合計関数でマッピングされるという考えです。

最初の述語は正の価格を確保するためのもので、2 つ目は ID の一意性を確保するためのものです。つまり、ドメインをまだ割り当てられていないすべての整数に減らします。これが正しいとは思いませんが。

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:

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:

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!

現在、CreditCard クラスの object-Z 仕様の例を実行しようとしていますが、可視性リストと INIT スキーマを宣言するときに問題が発生しました。これを修正する方法はありますか? 読んでくれてありがとう

可視性リストは、アイテムがクラスの機能ではないことを示しています

未申告の名前: バランス

Z表記を使用して論理式を証明しようとしています。しかし、私は Z 言語は初めてです。上記の論理式の証明を教えてください。