問題タブ [z-notation]

私はちょうど大学の授業を思い出していて、プロの環境で「Z表記法」を使用した人がいるかどうか知りたいと思っていました. 正直なところ、これまでの人生で参加したクラスの中で最も退屈なクラスだったと言わざるを得ません。先生のせいかもしれませんが、当時はみんな本当に時間の無駄だと思っていました。聞き間違いかもしれないので、教えていただきたいです。

それまたは派生言語 (Z++) を使用している場合は、それがどのように役立つかを知りたいと思います。Z またはあなたのアプリケーションのいくつかの一般的に知られているアプリケーションを知りたいだけです。

よく知らない人のために: http://staff.washington.edu/jon/z/z-examples.html

LyX で Zed Notation スキームを作成することは可能ですか? どうすればそれができますか？

Z仕様の記述をサポートするLaTeX用のパッケージはありますか? スキーマの水平形式と垂直形式の両方に興味があります。

ウィキでこれら2つの概念の定義を読みましたが、違いはまだ明らかではありません。誰かが例といくつかの簡単な説明を与えることができますか？

私はZ表記の完全な初心者です。Z でグラフ タイプを表す必要があります。私が考えているのは、ノードとエッジの間を簡単に自由に移動できるように、インシデンス マトリックスを使用することです。

唯一の問題は、Z で入射行列を指定する方法がわからないことです。私は 2D 配列が必要だと思いますが、Z 表記に使用できる参照資料を調べると、配列は一般的に seq を使用して表されます。多次元配列を指定する別の方法はありますか?

前もって感謝します。

UML を Z 表記に変換 (形式化) する方法はありますか? つまり、UML 要件を z のような正式な言語に書き直す方法はあるのでしょうか?

私の悪い英語で申し訳ありません。私の母国語は英語ではありません。ありがとうございました。

これがオーバーフローに属していない場合は申し訳ありませんが、今年の大学で Z を学ぶようになったので、Z を使用して仕様を作成し続けたいという強い衝動があります。

LinuxまたはSunOSで通常使用されていることを現在理解しているため、Mac PCでダウンロードできるかどうかを知りたかったのですが、自宅にはどちらもありません。グーグルで見つけられなかったので、ダウンロードできる場所へのリソースを大いに感謝します。zans animator と ztc type checker もインストールしたいです。

前もって感謝します。

以下を受け入れる操作 Bus_Arrives があります

LINE、BUS_ID、BUSROAD

• ある路線のバスが駅に到着し、空いているバス道路が割り当てられます。それ以外の場合はキューに入ります。

--------New_Bus_Arrives--------------------------------------------- -------------------------------------------------- ----

| | △バス停

| | バスライン?: LINE

| | バス?: BUS_ID

| | br?: バスロード

==============================================

| | 前提条件はこちら（それをキューに追加するケースは実装されていますが、質問とは関係ないので追加しません。） 以下は、この操作が完了した後のシステムの変化です。

| | free' = free \ {br?}

| | routing' = ルーティング

| | 出発' = 出発 U {br? |--> バス?}

| | 訪問数 = 訪問数 U {br? |--> ルーティング(|ライン?|) }

私の質問は次のとおりです。たとえば、訪問が正しく表現されている場合は Z です。たとえば、ルーティング (回線?) リレーションが呼び出されると、一連のステーション要素 {station1,station2,station3} が返されます。ただし、これを訪問関係にマッピングして更新するときは、次のようにしています: br? {station1,station2,station3} にマップされます。これは可能ですか、それとも br と言わなければなりませんか? セットのすべての要素に個別にマップされます。また、この場合、Z ではどのように表されますか?

説明内容に関する追加情報:

ルーティング: 対応するバス路線ごとに、バスがそこに到着するために通過する駅は何ですか (つまり、8 号線は LA、NY、マイアミに移動します)。

ルーティング: LINE <--> STATION (関係)

free: 利用可能なバス路線。

free: Π BUSROAD (パワーセット)

出発: すべてのバスがどのバス路線から出発するか (例: A がバス AY123 を出発)。

出発: LINE --> BUS_ID (機能)

訪問: 現在バスが割り当てられているすべてのバス道路について、どの駅を訪問するか。バス道路には、バスが 1 つだけある場合と、利用できる場合があります。

訪問: BUS_ROAD <--> STATION (関係)