Coqで独習するならどのページがいい？と聞かれたときのメモ - 簡潔なQ
Download Coq(英語) ダウンロードしなければ何も始まらない。 Download | The Coq Proof Assistant ちなみにLinuxディストリならcoqideパッケージをインストールするのが吉 Coqの入門記事を書く会 そこそこ体系的な入門サイト 2010-09-02 - ひとり勉強会 2010-09-14 - ひとり勉強会 2010-09-19 - ひとり勉強会 2010-10-12 - ひとり勉強会 Coq 99 練習問題。直観主義論理における有名な証明を一通り解ける。 Functional Programming Memo: [Coq] Coq-99 : Part 1 anarchy proof 練習用サイト。途中から一気に難化するのが問題。 わからなかったら他の人の解答も見られる anarchy proof - Curry-Howard Isomorp
にわとり小屋でのプログラミング日記
この記事はTppMark11の問題をCoqでやってみたという内容である。 問題はこちら: docs.google.com 命題論理式と同値であることの定義 命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Term) | Impl(t1: Term)(t2: Term) | TRUE | FALSE . 同値であることの定義 変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。 Fixpoint eval ctx t : bool := match t with | Var v => ctx v | Neg t => negb (eval ctx t) | And t1 t2 =>
プログラムに証明が付く日 | RANDMAX
この記事は「Theorem Prover Advent Calendar 2013」6日目の記事です。 http://qiita.com/advent-calendar/2013/theorem_prover 神田「野らぼー」にて、地下の薄暗い店内で… 「そう言えばこないだ隣で起こってたポインタオーバーラン、対応大変そうだったですけどちゃんと家に帰れてたんでしょうかね、新婚なのに…」 「ヌルポとかポインタオーバーランとか、どうして無くならないんだろうね。その時はみんな手を抜いてるつもりなんて毛頭なくて、一生懸命考えて大丈夫だと思ってるはずなんだけどね。レビューもして、それでも起こった後でみんなでソース見てみると、なんで気づかなかったんだよ！ってことになる。」 「人間って、そういうの苦手なんでしょうねきっと。ほら、『何かほかにありませんか』って聞かれても出てこないじゃないですか。静的な解析っ
Private Presentation
Private content!This content has been marked as private by the uploader.
目次一覧
■ 目次一覧 ホーム > 目次一覧 ■ 第1章 プログラムの正しさ —プログラムの検証入門— プログラムの正しさ プログラムの正当性とその証明法 —帰納的表明法— 検証条件 プログラムの停止性 演習問題 ■ 第2章 Floyd-Hoare 論理 Floyd-Hoare 論理 配列要素への代入文 演習問題 ■ 第3章 仕様としての事前条件と事後条件 配列の整列プログラム 配列を用いるプログラムの部分的正当性の例 仕様記述の例 演習問題 ■ 第4章 VDM-SL による仕様記述の例 簡単な仕様記述の例 有用な基本データ型 演習問題 ■ 第5章 例題で見るシステム仕様記述 住所録システム 参加登録システム 演習問題 ■ 第6章 事例で見る実用的仕様記述 対象とする自動販売機 自動販売機の抽象モデル モデルの拡張 ： ランプの導入 具体化 ： ボタンとカラムの導入 演習問題 ■ 付録A VDM-S
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
プログラム仕様記述論