15

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

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

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

4

6 に答える 6

3

Bメソッド( http://en.wikipedia.org/wiki/B-Method )を確認する価値があります。これは、Zのもう少し実用的な子孫です。アイデアは、(舞台裏に隠れている定理証明者の助けを借りて)改良手順を通じて実際に一連の証明義務を履行し、最終的に仕様から直接コードを生成できるということです。多くの「現実世界」のプロジェクトで使用されていると思います。

于 2010-05-15T22:41:48.340 に答える
3

Z は(ご指摘のとおり)仕様表記であり、正式な検証を容易にすることを目的としたプログラミング言語ではありません。

この表記法を使用して指定された大規模な (公に知られている) プロジェクトの 1 つは、Mondex スマート カード プラットフォームで使用されるプロトコルでした。最近では、元の Z 仕様の検証を含む複数のチームによる機械的チェックを使用して、元のマニュアル プルーフの正確性を判断する復活がありました。当然のことながら、多くの仮定がほとんどのチームによって無効であることが示されましたが、新しい根本的なエラーは検出されませんでした。

National Security Agency Tokeneer プロジェクトは、Spark Ada サブセットでの実装前に Z で指定されました。

表記の表現力を考えると、それが拡張される可能性は低いです。これはまた、証明をより複雑にし、非生産的になります。

于 2010-05-19T20:47:02.263 に答える
2

XCB( X11の元のXlib APIの代替品)がZ表記で正しいことが証明されたことを読んだときに、最初にZ表記に遭遇しました。

于 2010-05-13T02:09:15.497 に答える
2

Web サービス記述言語 (WSDL)は、Z 表記を使用して開発されました。Z 表記の仕様はhttp://www.w3.org/TR/wsdl20/wsdl20-z.htmlにあります。仕様書には、

Z 記法は、コンポーネント モデルを定義する規範テキストの品質を向上させ、テスト スイートがコンポーネント モデルによって暗示されたすべての重要なルールを確実にカバーするのを助けるために使用されました。

于 2014-12-18T22:08:42.610 に答える
0

私はユニでZをしなければなりませんでした!Linuxをインストールしている場合は、このアプリケーションCADiZを試してみてください...

于 2009-07-14T07:38:38.417 に答える
0

「Z++」はobject-Zと呼ばれます。私は 90 年代初頭以来 Z に積極的に取り組んでいない (CADiZ の Windows ポートに部分的に取り組んでいましたが、これは消滅したようです) ので、現在のコミュニティかどうかはわかりませんが、最近の論文がいくつか公開されています。object-Z を使用して UML を形式化します

于 2010-05-19T21:23:33.720 に答える