IIJ Research Laboratory
ネットワークの計測と解析 インターネットの使われ方やネットワークの挙動を把握する事は、ネットワークを運用し、その技術開発を行う ために欠かせません。しかし、観測で得られるデータ量は膨大ですがノイズが多く、また、観測できるのは極めて限られた部分でしかありません。そこで、膨大なデータから意味のある情報を抽出したり、部分的な観測からより一般的な傾向を推測する事が必要となります。... インターネット基盤技術 速くて、安全で、信頼性が高く、使いやすく、など、インターネットサービスへの要求はますます高まっています。これらの要求に応えるために、インターネットの 基盤技術も日々進歩しています。いまやインターネットはつながるだけのサービスではなく、高度で複雑な機能を備えた社会基盤となりました。IIJ技術研究所は、インターネットの基盤として実現が期待される機能を提供するために、さまざまな技術課題に取り組んで
Coqの入門記事を書く会 (2) - ひとり勉強会
第２回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。 実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同じ機能のものを簡単に作れてしまう「ユーザー定義命題」です（もちろん、共通のものがないと不便なので標準ライブラリで真っ先に定義されてますけど）。逆に言うと、もっと本格的なCoqコードで出てくる複雑そうな命題も、全部、「and」「or」「not」と同じユーザー定義型の仕組みで定義されてますので、「and」「or」「not」の扱いさえマスターすれば、他のどんなユーザー定義の命題の証明も同じ道具で書けちゃいますよ。
Software Foundations
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software. The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant. The exposition is intended for a broad range of readers, fro
Isabelle Tutorial その11 - caeruiro
5.7 Interlude: the Basic Methods for Rules 次の規則を例として、メソッドの作用を詳しく見ていきます。 規則の名前をRとします。 メソッドruleはQとサブゴールを単一化し、P1からPnを新たなサブゴールとします。 メソッドeruleはQとサブゴールを単一化すると同時にP1を前提の何れかと単一化し、P2からPnをn - 1個の新たなサブゴールとします。単一化した前提は除去されます。(rule R, assumption)は似ていますが、前提は除去されません。 メソッドdruleはP1を前提の何れかと単一化し、これを除去します。得られるサブゴールはP2からPnのn - 1個と、元のゴールの前提からP1とマッチした項を取り除きQを加えた、計n個です。 メソッドfruleはdruleと似ていますが、マッチした仮定を除去しません。 各メソッドに_tacを付け
Isabelle Tutorial その10 - caeruiro
5. The Rules of the Game この章ではIsabelleを使った証明のコンセプトとテクニックを紹介します。 5.1 Natural Deducation Isabelleでは、証明は推論規則によって構成されます。もっとも有名な推論規則の一つがmodus ponensです。 Isabelleでは自然演繹を使用します。Isabelleは適用可能な規則を探索することで、自動的に証明しようとします。自動証明がうまくいかない場合は、後述する方法で推論規則を適用し証明を手動で進めます。 5.2 Introduction Rules ある論理記号について、導入規則はその記号が含まれた式を推論するのに使用します。例えば論理積の導入規則は、もしPとQが言えるならば、P ∧ Qが言えることを示しています。 結論に論理積が導入されているのがわかります。多くの場合、Isabelleの証明は後ろ
Isabelle Tutorial その9 - caeruiro
3.4 Advanced Datatype 3.4.1 Mutual Recursion 相互再帰するデータ型の例として、算術式とブール式を示します。算術式には条件文が含まれており、よってブール式が含まれています。またブール式には値の比較が含まれており、よって算術式が含まれています。相互再帰するデータ型の定義はandで繋げて記述します。 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" | Sum "'a aexp" "'a aexp" | Diff "'a aexp" "'a aexp" | Var 'a | Num nat and 'a bexp = Less "'a aexp" "'a aexp" | And "'a bexp" "'a bexp" | Neg "'a bexp" この式の評価関数は次のように定義します。 prim
Isabelle Tutorial その7 - caeruiro
3.2 Induction Heuristics この節では、帰納法を使った証明のヒューリスティクスを説明します。最初は既に出てきたヒューリスティクスです。 再帰関数に関する定理は帰納法で証明せよ。 次は二つ以上の引数を取る関数の証明についてです。 i番目の引数が再帰的に定義されている関数は、i番目の引数について帰納法を適用せよ。 このヒューリスティクスは例えば2.3節の証明で使いました。 ゴールが固有的な場合、帰納ケースの前提が弱すぎて証明できない場合があります。そこでキーとなるヒューリスティクスは、帰納法を使う前にゴールを一般化することです。例を使って見ていきます。 関数revは効率が悪いので、累積変数を導入し線形時間で計算可能な関数を作成します。 primrec itrev :: "'a list => 'a list => 'a list" where "itrev [] ys =
Isabelle Tutorial その6 - caeruiro
3. More Functional Programming 3.1 Simplification 単純化はIsabelle及び他の多くのシステムにおいて重要な定理証明ツールです。今節では単純化について述べていきます。 3.1.1 What is Simplification? 簡単に言うと、単純化とは等式の左辺から右辺への変換を繰り返すことです。例えば、@のルールを使った単純化のステップを示します。 (0#1#[]) @ [] → 0#((1#[]) @ []) → 0#(1#([] @ [])) → 0#1#[] これは項書換えと見ることもでき、その場合等式は書換規則と見ることができます。 既に見たように単純化を用いて算術式を証明することもできますが、この場合は項書換え以上のことが行われています。ただしこれについてこのチュートリアルでは取り上げません。 3.1.2 Simplifica
Isabelle Tutorial その3 - caeruiro
2. Functional Programming in HOL ここからはHOLでどのように関数プログラムを書き、どのように検証するのか見ていきます。Isabelle/HOLを使う目的はシステムをモデル化し検証することなので、関数を実行可能なかたちで定義する必要はないのですが、まずは実行可能な定義を書くことにします。ただし、HOLでは必ず全域的でなければならないことに注意してください。 2.1 An Introductory Theory MLやHaskellと同じようにデータ型と関数を定義することができます。簡単なリストを定義しながら、方法を一つ一つ見ていきます。 theory ToyList imports Datatype begin HOLには既にリストが定義されています。多くの場合Mainをインポートしますが、定義済みのリストもインポートしてしまうため、ここではDatatype
チュートリアル - Alloy Analyzer で形式仕様記述
ここでは、Alloy で形式的に仕様を記述/検査する方法を簡単なものから段階的に説明していきます。 ボタンの仕様を書いてみよう 集合を使って仕様を書いてみよう 以降準備中
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
