問題タブ [z-notation]

z 記法パーサーまたはコンパイラーを見つける必要があります。できれば助けてください。

Objective-Z のアプリケーションは何ですか?

Objective-Z について読んだことがありますが、それが何に適用されるか想像できません。

この質問は広すぎるかもしれませんが、答えが多すぎるとは思いません。

「特定の定数が true の場合」(この場合は「sec=ok」の場合) の述語を記述しようとしています。その特定の結果の式を記述したため、述語は False と評価されます。述語の他の場所にある別の式と矛盾する含意。(f%^x ≠ g%^x) ∧ (f%^ci = g%^ci) は、x と ci の両方が普遍的に量化され、同じ型を持つという事実を考えると、矛盾するはずです。

ただし、Nitpick は、私が理解できない反例を生成します。誰かがこの補題を親切にチェックして、矛盾が証明できるかどうかを確認できることを望んでいました. または、どこが間違っているか教えてください。簡単な説明は次のとおりです。

• f と g は、任意の型 'a から 'b までの 2 つの部分関数です。

• 'sec' は、値が 'ok' と 'notok' の定数です。

  /li>

また、Function Application に関して、2 つの Z Math ツールキット間に「微妙な」違いがあることも確認しました。両方を試しましたが、問題は残ります。

Nitpick エラーはここで見ることができます http://i58.tinypic.com/316te1t.png

注: 参考までに、現在使用している部分関数の定義を HOL-Z から見つけてください。

私が見つけたすべての例には、宣言が 2 つしかありませんでしたsuch as name and date OR members and telephone。ただし、私のシナリオは次のとおりです。

AppointmentDB という Z スキーマを作成したいと考えています。AppointmentDB は、目的、出席者、スケジュールなどの予定の詳細を保持します

私の見解（編集済み）：

5 つの宣言と 1 つの述語があります。

ご覧のとおり、APPOINTMENT を他のすべての属性にリンクしようとしています。スキーマは正しいか完全か、またはさらに最適化するにはどうすればよいですか? また、述語部内で定義する関係から、どの関係を考えればよいかを知るにはどうすればよいでしょうか。

これは、予定 DB の Z スキーマです。

の名前に基づいて予定を見つける検索機能を作成したいと思いますattendees。

1. 検索機能が予定オブジェクトのすべての詳細を返すようにします。

どのように設計すればよいですか？

これが私の見解です：

Arrayスキーマのシーケンスを追跡するスキーマがありますData。Incrementプロモーションを使用して、 で使用する操作をプロモーションできArrayます。

ArrayIncrement内の 1 つのデータのみをインクリメントしますArray。ごと Dataにインクリメントするようにするにはどうすればよい\ran dataですか?