fm-forum @ ウィキ

fm-forum @ ウィキ内検索 / 「Coqインストール」で検索した結果

• Coqインストール
  Coqインストール Coqダウンロード先ページ Linuxの場合 Ubuntu または Debian の場合 # sudo apt-get install coq coqide ソースから最新版をインストールする場合 ソースからインストールするためにはocaml, camlp5が必要です。ソースにはREADMEの他にINSTALLというファイルがあって、そこにインストールするための詳細が記述されています。 OCamlがなければインストール (see http //ocaml.jp/インストール方法) camlp5のインストール (http //pauillac.inria.fr/~ddr/camlp5/からcamlp5-XXX.tgz をダウンロードする) $ ./configure --transitional $ make world.opt $ make ins...
• トップページ
  ...ooks Coq Coqインストール Coq参考資料 Certified Programming with Dependent Types関係 Coq命題論理の証明 Coqで数独 SPIN SPINインストール リンク集：関連しそうな話へのリンク集
• SPINインストール
  SPINインストール Macの場合 "% sudo port install spin"　でOKのはずだがインストールで失敗。失敗したパッケージを個々に"sudo port install -f package "で強制インストール。
• 20100310
  開催情報 日時：3/9 19 00-21 00 場所：銀座ルノアール新宿３丁目ビッグスビル店 2号室 定員：5名でとったけど10名まではいけまっせー。 http //atnd.org/events/3421 アジェンダ 今回からは、Coq(とできればEvent-B)を、ツールを動かしながら勉強していきます。 範囲を命題論理の証明だけに限定して、Coqに慣れましょう。 各自 Coq の実行環境をインストールしてきて下さい。　インストール方法(http //www39.atwiki.jp/fm-forum/pages/16.html) 　MacOS (Snow Leopard)とかLinuxの人はインストール手順を　Wikiに反映していただけると嬉しいです。 The Coq Proof Assistant, A Tutorial (http //www39.atwiki.j...
• 20100410
  開催情報 日時：4/10 13 00-19 00 場所：銀銀座ルノアールニュー大久保店 3号室 （東京都新宿区百人町1-18-8） 定員：10名でとったけど12名まではOK。 http //atnd.org/events/3687 アジェンダ 最終目標は形式手法を活用して仕事ができるようにすること！ まずは、考え方とツールに慣れるところから始めます。 初めての人にも導入資料へのリンクをお教えしますので、 レベル感を気にせず参加してください。 ただし、キャンセルは4/6 24 00までにお願いします （会議室料金は参加者で割り勘なので）。 Coqの題材：前回参加してなかった人が多かったので前回の復習からも検討。 各自 Coq の実行環境をインストールしてきて下さい。　インストール方法(http //www39.atwiki.jp/fm-forum/pages/...
• Coq参考資料
  Coq参考資料 教科書 "Interactive Theorem Proving and Program Development Coq Art The Calculus of Inductive" Springerから出版されているCoq本。良い本なのだが値段も高い。 Certified Programming with Dependent Types (http //adam.chlipala.net/cpdt/) Harvardの授業で使用 (PDF 360ページ程度)。定期的に改訂されている。 (Latest 2010/2/3) CPDTは関数型言語プログラマにとってCoqを理解しやすいいいテキストだと思います。 読む時は「Certified Programming with Dependent Types関係」も参照の事。 チュートリアル The...
• Certified Programming with Dependent Types関係
  Certified Programming with Dependent Types (CPDT)を読む為の前提 この教科書は、オリジナルなtacticのcrushというのを導入して、色々自動証明をさせています。なので、crush出来る様にしておかないと、教科書の証明を写経できません。crushを使う方法ですが、 Coqをインストールしておくのは当然。 CPDTの付属ファイルを入手する。詳しくはCPDT 1.6章を読むべきだが http //adam.chlipala.net/cpdt/cpdt.tgz をダウンロードする。 適当なディレクトリ (~/cpdt/とか)で展開し、makeする。 Coq起動時に、coqtop -I ~/cpdt/src とオプションでソースディレクトリを指定。 Coq内で、Require Import Tactics. と Tactics.v ...
• Coq命題論理の証明
  Coq命題論理の証明 命題論理の例題をtautoに頼らずに証明するためのTips 大まかなtacticを使う順序 大体、下記の原則で考える。 まずgoalをintroを使って分解して、goalを簡単にし、仮定を増やす事を考える。 goalが - の式の場合（演算子順序を考えると A - B の形の式と考えられる場合）は、intro, intros などを使えばOK、 goalが ~ の式（演算子順序を考えると ~X の形）の場合、goalがFalseになるまでintroして、「goal=Falseの場合」へ。 goalを導ける仮定がある場合（goalがAで、H X- A のような仮定がある場合）、apply H してgoalをXに変更する。 goal, 仮定の /¥, ¥/ は基本的には仮定の方から先に処理するのが楽だと思う。 仮定が H A /¥ B の形...
• Alloy
  Alloy UML2Alloy インストール方法 Alloy_4_Analyzerのページから。 MacOSXならdmgファイル入手。 他OSの場合、alloy4.jar を入手。 チュートリアル Tutorial_for_Alloy_Analyzer_4.0 がお薦めらしい。 Alloy_4_Tutorial_Materials というのもあり。 書籍 "Software Abstractions Logic, Language, and Analysis" は Alloy3 用なので、How_to_Update_the_Book_for_Alloy_4 を参照して訂正が必要。
• 20110305_14
  開催情報 日時：3/5 13 00-19 00 場所：豆蔵トレーニングルームB 参加者数：6名 アジェンダ ガリグ先生の今年のレポート課題をみんなで解く QCon Tokyo 2011で@kencoba と @yoshihiro503 がAlloy,Coq,SPINのお話をする ClojureでSimple Theorem Proverを実装してみた 元は"Programming Language Theory and Its Implementation"という本のCommon Lispの実装。 "Handbook of Practical Logic and Automated Reasoning"というOCamlを使う本もあるよ。 Clojureでオントロジー記述 社内でAlloy発表をしてみた 割と食いつきが良かった 「どうし...
• 第1回(2010/2/8)
  2010/2/8 第1会Formal Methods 勉強会 http //atnd.org/events/2968 Agendaトップエスイーチュートリアルセミナー「Bメソッドによる形式仕様記述」復習(小林健一) UMLからAlloyへ(小林健一) Coq and Why Formal Verification Tools(tmiya) http //homepage.mac.com/takashi_miyamoto/coq/Coq_20100208a.pdf http //www.slideshare.net/tmiya/coq-20100208a 勉強会名前決定 今後の進め方 今後の進め方Coqの勉強(http //adam.chlipala.net/cpdt/) B-Methodsの勉強(http //wiki.event-b.org/index.php/Event-B_Lang...
• 開催記録
  2010/2/8 第1会Formal Methods 勉強会 http //atnd.org/events/2968 Agendaトップエスイーチュートリアルセミナー「Bメソッドによる形式仕様記述」復習(小林健一) UMLからAlloyへ(小林健一) Coq and Why Formal Verification Tools(tmiya) http //homepage.mac.com/takashi_miyamoto/coq/Coq_20100208a.pdf http //www.slideshare.net/tmiya/coq-20100208a 勉強会名前決定 今後の進め方 今後の進め方Coqの勉強(http //adam.chlipala.net/cpdt/) B-Methodsの勉強(http //wiki.event-b.org/index.php/Event-B_Lang...
• 20100208
  2010/2/8 第1会Formal Methods 勉強会 http //atnd.org/events/2968 Agendaトップエスイーチュートリアルセミナー「Bメソッドによる形式仕様記述」復習(小林健一) UMLからAlloyへ(小林健一) Coq and Why Formal Verification Tools(tmiya) http //homepage.mac.com/takashi_miyamoto/coq/Coq_20100208a.pdf http //www.slideshare.net/tmiya/coq-20100208a 勉強会名前決定 今後の進め方 今後の進め方Coqの勉強(http //adam.chlipala.net/cpdt/) B-Methodsの勉強(http //wiki.event-b.org/index.php/Event-B_Lang...
• リンク
  リンク モデル検査によるソフトウェアテストの実践研究会 実践モデル検証 並行システムのモデル化と検証 ソフトウェア安全性のための論理検証技術 日本ユニシス技報「オブジェクト指向と形式仕様」 形式手法あれこれ SpecSharp(.Net上で動作する定理証明器 Coq クィックリファレンス 連絡先 Twitter http //twitter.com/kencoba kencobaの日記
• メニュー
  メニュー トップページ 勉強会 イベント 書籍 リンク 情報交換手段 メーリングリスト twitter @fm_forum_ ustream Skype 各形式手法資料 Alloy B-Method Coq Event-B ここを編集
• 20100429
  開催情報 日時：4/29 13 00-19 00 場所：銀座ルノアールビッグスビル店　2号室 参加者数：9名（飛び込みで入ってくれたみなさんありがとう！） アジェンダ Alloy(by ken.coba)Software AbstractionsのA Whirlwind Tourをみんなで実施する。 CEGAR(シガー) (by komagatimeさん)komagatimeさんによる解説 Coq(by tmiyaさん)CPDTを実施する。 コメント、質問 Blogで報告しました(tmiya) Fomal Methods Forum #4 どんどん追記してくださいな。
• 第2回20100310
  第2回20100310 チャレンジOCaml-Javaを使って、CoqのコードをJavaに変換してみる。
• イベント
  形式手法に関係したセミナー、勉強会、学会などありましたらどんどん追加してください。 イベント参加結果はぜひ、ご報告ください。 2010/8/29 Coq庵@名古屋 2010/8/23-30 2nd Asian-Pacific Summer School on Formal Methods@北京 2010/8/9-10 第二回層圏トポス合宿(8月9日-10日)@代々木オリンピックセンター 2010/7/11-14 ITP2010(Interactive Theorem Proving) 2010/7/12 13 00-17 00 Alloyセミナー@名古屋 2010/6/9-11 ソフトウェア・シンポジウム 2010 横浜 2010/5/12 形式手法徹底解説@ESEC 2010/4/29 第4回Formal Methods 勉強会 2010/4/25 Proof Cafe(栄) ...
• プラグイン/ニュース
  ニュース @wikiのwikiモードでは #news(興味のある単語) と入力することで、あるキーワードに関連するニュース一覧を表示することができます 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_174_ja.html たとえば、#news(wiki)と入力すると以下のように表示されます。 【グランサガ】リセマラ当たりランキング - グランサガ攻略wiki - Gamerch(ゲーマチ) 【まおりゅう】八星之紋章交換のおすすめ交換キャラ - AppMedia(アップメディア) Among Us攻略Wiki【アマングアス・アモングアス】 - Gamerch(ゲーマチ) マニュアル作成に便利な「画像編集」機能を提供開始！ - ナレッジ共有・社内wikiツール「NotePM」：時事ドットコム - 時事通信 マニ...
• プラグイン/人気商品一覧
  人気商品一覧 @wikiのwikiモードでは #price_list(カテゴリ名) と入力することで、あるカテゴリの売れ筋商品のリストを表示することができます。 カテゴリには以下のキーワードがご利用できます。 キーワード 表示される内容 ps3 PlayStation3 ps2 PlayStation3 psp PSP wii Wii xbox XBOX nds Nintendo DS desctop-pc デスクトップパソコン note-pc ノートパソコン mp3player デジタルオーディオプレイヤー kaden 家電 aircon エアコン camera カメラ game-toy ゲーム・おもちゃ全般 all 指定無し 空白の場合はランダムな商品が表示されます。 ※このプラグインは価格比較サイト@PRICEのデータを利用しています。 ...
• プラグイン/コメント
  コメントプラグイン @wikiのwikiモードでは #comment() と入力することでコメントフォームを簡単に作成することができます。 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_60_ja.html たとえば、#comment() と入力すると以下のように表示されます。 名前 コメント
• まとめサイト作成支援ツール
  まとめサイト作成支援ツールについて @wikiにはまとめサイト作成を支援するツールがあります。 また、 #matome_list と入力することで、注目の掲示板が一覧表示されます。 利用例）#matome_listと入力すると下記のように表示されます #matome_list
• プラグイン
  @wikiにはいくつかの便利なプラグインがあります。 アーカイブ コメント ニュース 人気商品一覧 動画(Youtube) 編集履歴 関連ブログ これ以外のプラグインについては@wikiガイドをご覧ください = http //atwiki.jp/guide/
• プラグイン/動画(Youtube)
  動画(youtube) @wikiのwikiモードでは #video(動画のURL) と入力することで、動画を貼り付けることが出来ます。 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_209_ja.html また動画のURLはYoutubeのURLをご利用ください。 ＝＞http //www.youtube.com/ たとえば、#video(http //youtube.com/watch?v=kTV1CcS53JQ)と入力すると以下のように表示されます。
• 書籍
  和書 形式手法の技術講座 (佐原伸/SRC) VDM++ プログラム仕様記述論 (荒木啓次郎/オーム社) VDM-SL, Z ソフトウェア科学基礎 Bメソッドによる形式仕様記述 SPINモデル検査―検証モデリング技法 (中島震/近代科学社) SPIN 形式手法モデル理論アプローチ (高原康彦 他/日科技連) MTA-SDK ディペンダブルシステム SPINによる設計モデル検証 (吉岡信和 他/近代科学社 TopSE) SPIN 4日で学ぶモデル検査 (初級編) (産業技術総合研究所システム検証センター/NTS) NuSMV, SPIN; KNOPPIX CD-ROM付 組み込みソフトウェアの設計 検証 ソフトウェア開発のモデル化技法 (J.フォッツジェラルド/P.G.ラーセン/岩波) VDM-SL 組み込みソフトウェア2007 モデルに基づく開発方法論の全て (日経BP) 日経エレクト...
• プラグイン/編集履歴
  更新履歴 @wikiのwikiモードでは #recent(数字) と入力することで、wikiのページ更新履歴を表示することができます。 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_117_ja.html たとえば、#recent(20)と入力すると以下のように表示されます。 取得中です。
• プラグイン/アーカイブ
  アーカイブ @wikiのwikiモードでは #archive_log() と入力することで、特定のウェブページを保存しておくことができます。 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/25_171_ja.html たとえば、#archive_log()と入力すると以下のように表示されます。 保存したいURLとサイト名を入力して"アーカイブログ"をクリックしてみよう サイト名 URL
• プラグイン/関連ブログ
  関連ブログ @wikiのwikiモードでは #bf(興味のある単語) と入力することで、あるキーワードに関連するブログ一覧を表示することができます 詳しくはこちらをご覧ください。 ＝＞http //atwiki.jp/guide/17_161_ja.html たとえば、#bf(ゲーム)と入力すると以下のように表示されます。 #bf
• @wiki全体から「Coqインストール」で調べる

更新順にページ一覧表示 | 作成順にページ一覧表示 | ページ名順にページ一覧表示 | wiki内検索