Software Foundations 日本語版WikiSoftware Foundations日本語版Wikiへようこそ Software Foundationsは、米国ペンシルバニア大のBenjamin Pierce先生のグループによって作成・公開されている、プログラミング言語Coqに沿ったソフトウェア作成についてのドキュメントです。 ここはその日本語版作成に集まった有志が情報を交換する場です。 日本語版の公開にあたって、Pierce先生のご了解をいただいています。
Coq Party - rfなブログ
11/27 に、Coq Partyに参加してきました。 資料などはこちら。 エンジニア・ミーツ・Coq すぐ分かる形式手法 形式手法とは？ 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法 仕様化の正しさは終盤のシステムテストまで分からない 結合テストでバグが「こんにちは！」 手戻りコストがとても大きい V字モデルは横軸工程、縦軸は「開発の詳細さのレベル」 ソフトウェア開発の不具合の半数は上流工程 その半分は下流工程まで見つからない 上流時点で「厳密で、間違い、漏れ、抜け、矛盾の無い仕様」が必要 仕様は自然言語で書かれているため、あいまい or/xor 問題や、if/iff 問題 など 自然言語ではなく、形式的な仕様記述が必要 形式手法 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う 数学ベースの厳密な定義 形式仕様は仕様の記述の形式化 プログラムではな
Coq クィックリファレンス
Coq クィックリファレンス 書きかけだけれど、たぶん永遠に書きかけなので、とりあえず書いたところだけ公開。 基礎知識 Gallina の構文と Vernacular コマンド オプション モジュール Prop vs. Set vs. Type タクティク リファレンス 証明の補助: idtac, fail, move, clear, set, remember, pose, rename, intro, assert, cut, lapply, specialize, generalize 項による証明: exact, refine, apply 否定と矛盾: absurd, contradict, contradiction 帰納法と場合分け: fix, cofix, elim, induction, case (case_eq), destruct, intros, decompos
Coq 証明事例集: ゴールが……のとき
証明事例集: ゴールが……のとき 以下の例では、全て予め Parameters P Q R : Prop. を実行してあるものとする。 ゴールが前提に等しい場合 前提がゴールに等しい場合を参照。 ゴールが含意の場合 (P -> Q の形) およびゴールが全称量化子 (forall) の場合 intro または intros で含意の仮定を前提に移動する。 Coq < Goal P -> P. 1 subgoal ============================ P -> P Unnamed_thm < intro H. 1 subgoal H : P ============================ P ゴールが代数的データ型の場合 ゴールの型が代数的データ型の場合は、適当なコンストラクタを適用する。コンストラクタが引数を取る場合は、それが新たなゴールとなり得る。 ゴールが
プログラム定理証明 - 有限会社ITプランニング(IT Planning Inc.)
プログラム定理証明 弊社での、プログラム定理証明を用いたソフトウェア品質保証の取り組みについて紹介します。 iZE Smart Desktopミドルウェアの正しさ検証 (ソフトウェア科学会PPL2010においてポスター発表、TPP10にて発表) (有)ITプランニングは(株)アイズの「スマートデスクトップ・クライアント」の一部モジュールを請負開発し，その際証明支援器Coqを使用した． 本プロジェクトではD-Busで扱うデータとJSONとの相互変換に関して静的検証を行った． 具体的には，検証対象とする関数をCoqで定義した上で諸性質を証明し，Extract機能により全体のOCamlのプログラムと協調させるという方法を用いた． 今回行った検証の詳細と，実際にCoqを開発現場で使う上で行った工夫などを報告する． (PPL2010予稿集より) プログラム定理証明って？ プログラム定理証明は、プログ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
