Coqの入門記事を書く会 (4) - ひとり勉強会
今回は、入門記事書きはちょっと休憩して、Coqの解説記事などを集める会です。 英語 言語そのものを浅く/深く眺めていく、という方向のテキスト３つ： Coq in a Hurry 「忙しい人のためのCoq入門」。比較的よくまとまっている気がしました。 Coq Proof Assistant： A Tutorial 本家のチュートリアル Interactive Theorem Proving and Program Development (Coq'Art) Amazon 定番の一冊 講義の素材として作られたチュートリアル達。より具体的な題材での演習付きなので面白いかも： 2nd Asian-Pacific Summer School on Formal Methods Using Proof Assistants for Programming Language Research or, H
形式手法の考え方 | 形式手法実践ポータル
このページでは，形式手法の基本的な考え方を説明します．形式手法と分類される様々な手法に共通する考え方として，数理論理学等に基づき，システムの注目する側面を正確に，曖昧さのない形で表現します．これによりシステムへに関する理解を明確にするとともに，システムの満たす性質について科学的・系統的な分析や検証をツールを用いて行います． 形式手法が効くところ ソフトウェア開発の過程においては，システムや個々のコンポーネント，メソッド等が「何を（どれだけうまく）すべきか」，そしてそれらが「求められているものをどうやって実現するのか」を議論し定めていきます．開発の初期過程では要求仕様という形で前者の「何をするのか」といったことを主に議論し，徐々に「どう実現するのか」を具体化・詳細化していき，最終的なプログラムを得ることとなります． 「何をすべきか」や「どう実現するのか」という情報は，開発の様々な段階（要求，
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
