Software Foundations 日本語版WikiSoftware Foundations日本語版Wikiへようこそ Software Foundationsは、米国ペンシルバニア大のBenjamin Pierce先生のグループによって作成・公開されている、プログラミング言語Coqに沿ったソフトウェア作成についてのドキュメントです。 ここはその日本語版作成に集まった有志が情報を交換する場です。 日本語版の公開にあたって、Pierce先生のご了解をいただいています。
Krakatoa and Jessieを用いた、Javaプログラムの正当性＆安全性証明(アルゴリズムもあるよ！) - 簡潔なQ
概要 Javaプログラムに専用の記法で満たすべき条件を形式的に記述し、それをCoqの問題に変換して手動で証明する。 この記事はCompetitive Programming Advent Calendar 2011およびTheorem Proving Advent Calendar 2011の12日目の担当記事である。 用意するもの Why 2.30 および Why3 0.71 (両方必要) Why 2.30に同梱されているKrakatoa and Jessieを用いる。 Coq 上記ソフトウェアが動作するOS (ここではUbuntu 11.10) なお、Ubuntu上での準備方法は、直前の記事を参照。 流れ Javaコードに、KML(JMLをベースにした仕様記述言語)で仕様を付記する。 Krakatoaを使って、JavaコードをJessieコードに変換。(ちなみに、Cコード+ACSLをJ
Gappa
(Génération Automatique de Preuves de Propriétés Arithmétiques) Gappa is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act
Certified Programming with Dependent Types
This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation. I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since s
2007-04-01から1ヶ月間の記事一覧 - 菊やんの雑記帳
δ-reduction δ-reduction は変数をその定義で置き換える。まず何か定義して、 Coq < Definition hoge := fun x:nat => 2+x. hoge is definedcbvを実行してみる。 Coq < Eval cbv delta [hoge] in (hoge 3). = (fun x : nat => 2 + x) 3 : natこの場合は「hog…
Coq - PukiWiki
雑多な文書 † Coq/install インストールのしかた(cygwin+Meadow) Coq/tactics tactic の中途半端な解説 Coq/Proofs? 証明したこと
ProofGeneral Coq-mode - suer のブログ
ProofGeneral で Coq を使う． Coq のインストール方法はハイテンションなインストール記事にまかせるとします． この記事みたいにハイテンションにインストール記事を書こうかとも思ったけどレベルが高すぎます． Mac にウインドウズ・ベロは無いしw Mac 版はパッケージから入ります． 困ったのは ProofGeneral 3.5 は Mac 上の Coq と通信すると，なぜかフリーズします． ためしに Development Ver. を使ってみるとうまく動きました． なんで? インストール上記サイト(Development)から開発版の最新をダウンロードします． 解凍すると，本体ディレクトリと本体ディレクトリへのProofGeneralというシンボリックリンクが現れます． 設定;; ProofGeneral (load-file "{展開して現れたProofGeneral
OCamlerのためのCoq便利モジュールを公開してみた - にわとり小屋でのプログラミング
このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。 ダウンロード: http://sourceforge.jp/projects/coqbase/ 具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を使った型安全なprintf関数 natからOCamlのint、stringからOCamlのstringへの相互変換関数 Coqでのbool、sumbool、list、option型をそのままOCamlの型として使うための連携
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
