最初の証明

十分 · 三つの手順 · 信頼を前提にするものは何もありません

これは初心者向けの道です。プログラマーである必要はなく、アカウントも 不要で、あなたが存在することを私たちに知らせる必要もありません。この 道の終わりには、あなた自身のコンピュータが——私たちのものではなく、 私たちの言葉によってでもなく——ライブラリにある実際のルールの背後に ある数学を確認し終えているはずです。

すでにプルーバーの扱いに慣れている方には、 完全な手順がさらに先まで進みます: フロントのビルドと、真理値表の全行の確認です。このページは証明の ところで止まります。そこが最も重要な部分であり、また、何もインストール する必要のない部分だからです。

これから確認すること

このルールはbrief-fill policyと呼ばれています。 アシスタントが、所有者に尋ねる代わりに、所有者に代わって答えてよいのは いつかを決めるものです。これについて四つの主張がなされており、その 四つすべてが、これからあなたのマシンでテストされます:

• それを許可するルールなしに、答えを埋めることは決してない。
• ルールストアが存在しない場合、何も通さない。
• 何も発明しない。
• ルールがすでに答えていることを、あなたに尋ねることは決してない。

これらはブログ記事の中の約束ではありません。定理であり、これから プルーバーがそれを破ろうと試みます。

手順1 — プルーバーを入手する

これは無料であり、私たちのものでもありません — 私たちからでは なく、Adaコミュニティから来ています。それが重要な点です。私たちの 仕事を確認するものが、私たちがあなたに手渡したものであってはならない のです。

手順2 — ルールを入手する

最初の実行では、チェックサムは無視してかまいません — 手順3の 証明はそれに依存しません。これは、受け取ったファイルが私たちの公開 したファイルと同一であることを確認したいときのためにあり、 the catalogueが示しているのと同じものです。

手順3 — あなたのコンピュータに確認させる

展開したフォルダでターミナルを開き、次の二行を実行してください:

cd brief-fill-policy/core/src
gnatprove -P proof.gpr -f -U --level=2

待ちます。終わったら、次の二語を探してください:

0 unproved

それだけです。それが演習のすべてです。 他に何も インストールする必要はなく、この手順は他に何も入っていない素の マシンでも動きます — ダウンロードしたプルーバーが、証明に必要な ものすべてを持っているからです。

たった今起きたこと

あなたのコンピュータは、上記の四つの主張を受け取り、そのいずれかが 成り立たないケースを探そうとして、見つけられませんでした — そんな ケースが存在しないからです。「テストしてみたら、うまくいったようだ」 ではありません。「メンテナーがそう言っている」でもありません。言い くるめることのできない機械が、反例を探しに行き、何も持たずに戻って きたのです。

あなたは、それを私たちが言うことを信頼したわけではありません。 あなたは、自分が所有するハードウェアの上で、それが起こるのを見た のです。

任意 — わざと壊してみる

あと五分あるなら、やってみる価値のある部分です。「はい」としか 言わない確認には、大した価値がないからです。

任意のテキストエディタでbrief_fill_policy_pkg.adsを開き、 ストアが存在しない場合でも答えが通ってしまうよう、ルールを変更して ください。同じコマンドをもう一度実行します。プルーバーは拒否します — そして、あなたがたった今破った、まさにその定理の名前を挙げます。

その拒否こそが、セキュリティモデルのすべてです。Ghillieは、これに 通らないものを一切インストールしません。つまり、あなたがたった今 手作業で行ったことを、彼はあなたに代わって毎回行っているのです。

これが証明しないこと

後になってあなたが気づくよりは、私たちから先にお伝えしておきたいと 思います。証明が対象とするのは判断ルールです — 誰が何を 見てよいか、何が外に出てよいか、届いたものが何を満たさなければならない か。それ以外のソフトウェアが魔法になるわけではありませんし、私たちは そうだと主張してもいません。その正直さが約束であり、それが約束の すべてです。

次に行く場所

• 完全な手順 — フロントを ビルドし、出荷された真理値表の全行を確認します。
• The catalogue — 棚に残る他のすべて。 どの一品も、同じ方法で再導出できます。
• Ghillie — これらのルールが仕える アシスタントです。
• The Reef machine — この ページより先に進みたい場合に必要なハードウェアです。

うまくいかなかった場合、それも一つの知見です。ぜひお聞かせ ください。説明のつかない拒否のほうが、成功よりも私たちにとって 興味深いものです。