研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む
#TPP2014 高信頼な理論と実装のための定理証明および定理証明器
研究集会 「高信頼な理論と実装のための定理証明および定理証明器」 高信頼なソフトウェア開発のために必要な形式手法, ソフトウェア検証, 数学の形式化, および, 証明の計算機による検証に関する研究集会を九州大学西新プラザで開催します. 続きを読む
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
Why: asoftware verification platform
Overview Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. (See the list of supported provers below.) Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, s
はてなブログ | 無料ブログを作成しよう
うめぇヨーグルトソースでもいかがですか。個人差にもよりますが。もしよろしければ。 お久しぶりです。 最近うんめぇ〜と思ってるヨーグルトソースがあるので、書いていこうと思います。 ヨーグルトとハーブ類をもりもり使うので、そういうのが食べられない方にはうんめぇソースではないです。ごめんなさい…。もしよろしければお茶だけも…旦~ 【用意する…
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 その8 - caeruiro
3.3 Case Study: Compiling Expressions 今節では、変数、定数、そして二項演算子からなる式からスタックマシーンへのコンパイラを開発します。これは、2.5.6のブール式を一般化したものです。変数や値の型は特に定めず、型パラメータとして定義します。二項演算子も詳細は定めず、適当な演算子を持っているとします。 types 'v binop = "'v => 'v => 'v" datatype ('a, 'v) expr = Cex 'v | Vex 'a | Bex "'v binop" "('a, 'v) expr" "('a, 'v) expr" 三つの構成子は定数、変数、二項演算子の適用を表わします。式をある環境の下で評価する関数は次のように定義できます。 primrec "value" :: "('a, 'v) expr => ('a => 'v) =
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 その5 - caeruiro
2.6 Some Basic Types 2.6.1 Natural Numbers 自然数を表す型natは構成子0とSucで定義されています。case式を使った例を示します。 case n of 0 => 0 | Suc m => m 原始再帰関数の定義と、帰納法による証明の例も示します。 primrec sum :: "nat => nat" where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" lemma "sum n + sum n = n * (Suc n)" apply(induct_tac n) apply(auto) done +, -, *, div, mod, min, max, <=, <などが定義されています。最小値演算LEASTも定義されています。例えば(LEAST n. 0 < n) = Suc 0です。 定数0や1
Isabelle Tutorial その4 - caeruiro
やっと証明に入りました。 2.3 An Introductory Proof 証明の大まかな流れを追ってみます。 Main Goal. リストにrevを二回適用すると元に戻ることを証明します。 theorem rev_rev [simp]: "rev (rev xs) = xs" theoremは新しい定理"rev (rev xs) = xs"を証明します。定理にはrev_revという名前を付けています。[simp]はこの定理を後から単純化ルールとして使うことを示しています。これは、単純化の際にrev (rev xs)をxsに置き換えることを意味します。定理名と単純化の属性はオプションです。 これを入力すると、Isabelleは次を返します。 1. rev (rev xs) = xs 証明中は、証明すべき残りのサブゴールが示されます。もちろん最初は単にメインゴールが示されます。 再帰関数に
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 -
入手方法 The Alloy Analyzer - http://alloy.mit.edu/ 機能 モデル解析ツール。 一階述語論理を元にした独自のモデル記述言語によりシステムの仕様を記述することで、その仕様に矛盾や漏れがないか、制約を満たさないような反例はあるか、などを分析・検査することができる。 基本構文 モジュール ファイルの先頭で指定する。 module ファイルパス/モジュール名 モジュールの定義 open ファイルパス/モジュール名 モジュールの参照 シグネチャ（型） Alloyのモデルは述語論理で表現される 論理式中の変数は必ずシグネチャ（signature）を持ち、sigキーワードにより定義される sig Person{} Person（人間）という型を定義 シグネチャはオブジェクト指向言語と同じように、継承することで差分的に定義できる。 sig Man, Woman e
チュートリアル - Alloy Analyzer で形式仕様記述
ここでは、Alloy で形式的に仕様を記述/検査する方法を簡単なものから段階的に説明していきます。 ボタンの仕様を書いてみよう 集合を使って仕様を書いてみよう 以降準備中
Alloy Analyzer で形式仕様記述
仕様を形式的に記述/検査することのできる言語やツールは、VDM, B, Z, Isabelle など他にも色々ありますが、 Alloy はそれらにくらべてより軽いフットワークで記述/検査することができるツールです。 それらのツールと Alloy との比較も、機会があればご紹介したいと思います。 2. Alloy を使った形式仕様記述の特徴 数理論理学＋集合論をベースとした Alloy の言語で仕様を記述します。 書いた仕様を、簡単に検査することができます。 難しい論理式の証明などは必要ありません。 検査結果は図で表示してくれるので、結果を目視で直感的に理解することができます。 仕様で書いた振る舞いをシミュレーションすることができます。 3. このページのスコープ ここでは仕様のうち、概要レベルの仕様や、重要な部分だけを抜き出した仕様といった、抽象度の高い仕様をスコープとしています。 抽象度
Isabelle Tutorial その2 - caeruiro
1.4 Variables もちろんIsabelleは自由変数と束縛変数を区別しますし、束縛変数は名前の衝突が起こらないよう自動で改名されます。この2つに加えて、?で始まる変数があります。これをスキーマ変数(schematic variable)またはアンノウン(unknown)といいます。スキーマ変数は論理的には自由変数と同じですが、Isabelleの証明では自由変数とは異なり他の項に置き換えることができます。 証明を終えるとその定理に含まれる自由変数がスキーマ変数に置き換えられることがわかります。これにより、新たな定理を他の定理の証明に使うことができるのです。実際に証明をしてみると、なんとなくわかってくるかと思います。ただし、スキーマ変数を意識する必要はあまりないでしょう。 1.5 Interaction and Interfaces Isabelleとshellで直接対話することもで
Isabelle Tutorial その1 - caeruiro
1. The Basics 1.1 Introduction Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。 1.2 Theories Isabelleを使用して理論を構築していきます。理論とは、型、関数、定理の集まりです。理論Tを定義するには次のように書きます。 theory T imports B1, ..., Bn begin 宣言、定義、証明などなど end B1, ..., Bnは既存の理論で、Tをこれらの上に構築していきます。オブジェクト指向プログラムのクラスの継承みないなものです。名前が衝突する場合は、T.fやB.fなどと書いて回避します。ファイル名はT.thyとします。 既存の理論ファイルは次のページで探すことができますし、Isabelleをインストー
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
イベントレポート：「ProofSummit2011」
【トップエスイーチュートリアル】 Coqで学ぶ定理証明入門 | topse.or.jp