OUnitドキュメント日本語訳 — OUnitドキュメント v1.1.0 documentation
また多くのサンプルもあります。 OUnitのexamplesディレクトリにあるもの example.ml test_stack.ml OASIS テスト あなたのプロジェクトやサンプルをここに追加したい場合は 機能リクエスト をしてみましょう お探しの情報が見つからない場合は、検索機能やインデックスから探してみて下さい。 Index Module Index Search Page 翻訳について¶ このドキュメントは、OUnitのドキュメント (http://ounit.forge.ocamlcore.org/) の内容を参考に翻訳しています。また、必要に応じて、配布物の中のファイルなども引用しながら訳しています。
なぜ次に学ぶ言語は関数型であるべきか - YAMAGUCHI::weblog
はじめに こんにちは、Python界の情弱です。ちょっと前にOCaml系のエントリを色々と眺めていたらYaron Minsky氏のエントリを見つけたので翻訳してみました。 OCaml for the Masses - ACM Queue Yaron Minsky氏はJane Streetで第一線で活躍されるエンジニアで、Jane Streetの技術ページをはじめ多くの場所でOCamlに関しての知見を語ってくださっています。 Jane Street Tech Blogs 本エントリはJohn Hughesの名エントリ「なぜ関数プログラミングは重要か」を受けてACM Queueに寄稿されたものの日本語訳です。 なぜ関数プログラミングは重要か Why the next language you learn should be functional YARON MINSKY, JANE STREE
Coqの入門記事を書く会 (2) - ひとり勉強会
第２回です。前回は「forall」と「->」の扱い方でした。今回は、「ならば (->)」以外の定番の論理演算、「and」「or」「not」のお話です。 実は、Coq の本当に言語組み込みの命題構成子は forall と -> だけで、「and」「or」「not」は、Coq使いなら自分で同じ機能のものを簡単に作れてしまう「ユーザー定義命題」です（もちろん、共通のものがないと不便なので標準ライブラリで真っ先に定義されてますけど）。逆に言うと、もっと本格的なCoqコードで出てくる複雑そうな命題も、全部、「and」「or」「not」と同じユーザー定義型の仕組みで定義されてますので、「and」「or」「not」の扱いさえマスターすれば、他のどんなユーザー定義の命題の証明も同じ道具で書けちゃいますよ。
Software Foundations
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software. The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a "proof script" for the Coq proof assistant. The exposition is intended for a broad range of readers, fro
第19回 アクターで楽々並行プログラミング(1)
有限会社ITプランニング勤務のプログラマー。Scala、OCaml、F#などの静的型付け関数型言語を利用したシステム開発業務に従事。定理証明支援器Coqやモデル発見器Alloyといった形式手法ツールの業務への応用にも興味を持っている。 Scalaの標準ライブラリは、Java程大きくありませんが、パーサーコンビネーターを筆頭に小粒でもぴりりと辛い逸品が揃っています。この記事でご紹介する「アクター」もその一つ、マルチスレッドのスパゲッティをおいしいペペロンチーノに変えてくれる、魔法のスパイスです。new Threadとしたくなったら、一歩立ち止まってscala.actorsパッケージの扉を叩いてみてください。 なお、本稿では2回にわたって、アクターとは何なのか、アクターを使うとどのような事が可能なのかをご紹介する予定です。並行処理に興味があったり、なんらかの形で並行処理に触れたりしたことがあれ
Exploring Lift</title> <meta name="Subject" content="The Lift Web Framework"> <meta name="Keywords" content="Lift Scala Web"> <meta name="Author" content="Derek Chen-Becker, Marius Danciu and Tyler Weir"> <meta name="Creator" content="LaTeX with hyperref
Exploring Lift Derek Chen-Becker, Marius Danciu and Tyler Weir August 18, 2010 ii Copyright © 2008, Derek Chen-Becker, Marius Danciu and Tyler Weir. This work is licensed under the Creative Commons Attribution-No Derivative Works 3.0 Unported License. Contents Contents iii List of Figures v List of Listings vii I The Basics 1 1 Welcome to Lift! 3 1.1 Why Lift? . . . . . . . . . . . . . . . . . .
Why: asoftware verification platform
Overview Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. (See the list of supported provers below.) Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, s
Isabelle Tutorial その11 - caeruiro
5.7 Interlude: the Basic Methods for Rules 次の規則を例として、メソッドの作用を詳しく見ていきます。 規則の名前をRとします。 メソッドruleはQとサブゴールを単一化し、P1からPnを新たなサブゴールとします。 メソッドeruleはQとサブゴールを単一化すると同時にP1を前提の何れかと単一化し、P2からPnをn - 1個の新たなサブゴールとします。単一化した前提は除去されます。(rule R, assumption)は似ていますが、前提は除去されません。 メソッドdruleはP1を前提の何れかと単一化し、これを除去します。得られるサブゴールはP2からPnのn - 1個と、元のゴールの前提からP1とマッチした項を取り除きQを加えた、計n個です。 メソッドfruleはdruleと似ていますが、マッチした仮定を除去しません。 各メソッドに_tacを付け
Isabelle Tutorial その10 - caeruiro
5. The Rules of the Game この章ではIsabelleを使った証明のコンセプトとテクニックを紹介します。 5.1 Natural Deducation Isabelleでは、証明は推論規則によって構成されます。もっとも有名な推論規則の一つがmodus ponensです。 Isabelleでは自然演繹を使用します。Isabelleは適用可能な規則を探索することで、自動的に証明しようとします。自動証明がうまくいかない場合は、後述する方法で推論規則を適用し証明を手動で進めます。 5.2 Introduction Rules ある論理記号について、導入規則はその記号が含まれた式を推論するのに使用します。例えば論理積の導入規則は、もしPとQが言えるならば、P ∧ Qが言えることを示しています。 結論に論理積が導入されているのがわかります。多くの場合、Isabelleの証明は後ろ
Isabelle Tutorial その9 - caeruiro
3.4 Advanced Datatype 3.4.1 Mutual Recursion 相互再帰するデータ型の例として、算術式とブール式を示します。算術式には条件文が含まれており、よってブール式が含まれています。またブール式には値の比較が含まれており、よって算術式が含まれています。相互再帰するデータ型の定義はandで繋げて記述します。 datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" | Sum "'a aexp" "'a aexp" | Diff "'a aexp" "'a aexp" | Var 'a | Num nat and 'a bexp = Less "'a aexp" "'a aexp" | And "'a bexp" "'a bexp" | Neg "'a bexp" この式の評価関数は次のように定義します。 prim
Isabelle Tutorial その8 - caeruiro
3.3 Case Study: Compiling Expressions 今節では、変数、定数、そして二項演算子からなる式からスタックマシーンへのコンパイラを開発します。これは、2.5.6のブール式を一般化したものです。変数や値の型は特に定めず、型パラメータとして定義します。二項演算子も詳細は定めず、適当な演算子を持っているとします。 types 'v binop = "'v => 'v => 'v" datatype ('a, 'v) expr = Cex 'v | Vex 'a | Bex "'v binop" "('a, 'v) expr" "('a, 'v) expr" 三つの構成子は定数、変数、二項演算子の適用を表わします。式をある環境の下で評価する関数は次のように定義できます。 primrec "value" :: "('a, 'v) expr => ('a => 'v) =
Isabelle Tutorial その7 - caeruiro
3.2 Induction Heuristics この節では、帰納法を使った証明のヒューリスティクスを説明します。最初は既に出てきたヒューリスティクスです。 再帰関数に関する定理は帰納法で証明せよ。 次は二つ以上の引数を取る関数の証明についてです。 i番目の引数が再帰的に定義されている関数は、i番目の引数について帰納法を適用せよ。 このヒューリスティクスは例えば2.3節の証明で使いました。 ゴールが固有的な場合、帰納ケースの前提が弱すぎて証明できない場合があります。そこでキーとなるヒューリスティクスは、帰納法を使う前にゴールを一般化することです。例を使って見ていきます。 関数revは効率が悪いので、累積変数を導入し線形時間で計算可能な関数を作成します。 primrec itrev :: "'a list => 'a list => 'a list" where "itrev [] ys =
Isabelle Tutorial その6 - caeruiro
3. More Functional Programming 3.1 Simplification 単純化はIsabelle及び他の多くのシステムにおいて重要な定理証明ツールです。今節では単純化について述べていきます。 3.1.1 What is Simplification? 簡単に言うと、単純化とは等式の左辺から右辺への変換を繰り返すことです。例えば、@のルールを使った単純化のステップを示します。 (0#1#[]) @ [] → 0#((1#[]) @ []) → 0#(1#([] @ [])) → 0#1#[] これは項書換えと見ることもでき、その場合等式は書換規則と見ることができます。 既に見たように単純化を用いて算術式を証明することもできますが、この場合は項書換え以上のことが行われています。ただしこれについてこのチュートリアルでは取り上げません。 3.1.2 Simplifica
Isabelle Tutorial その5 - caeruiro
2.6 Some Basic Types 2.6.1 Natural Numbers 自然数を表す型natは構成子0とSucで定義されています。case式を使った例を示します。 case n of 0 => 0 | Suc m => m 原始再帰関数の定義と、帰納法による証明の例も示します。 primrec sum :: "nat => nat" where "sum 0 = 0" | "sum (Suc n) = Suc n + sum n" lemma "sum n + sum n = n * (Suc n)" apply(induct_tac n) apply(auto) done +, -, *, div, mod, min, max, <=, <などが定義されています。最小値演算LEASTも定義されています。例えば(LEAST n. 0 < n) = Suc 0です。 定数0や1
Isabelle Tutorial その2 - caeruiro
1.4 Variables もちろんIsabelleは自由変数と束縛変数を区別しますし、束縛変数は名前の衝突が起こらないよう自動で改名されます。この2つに加えて、?で始まる変数があります。これをスキーマ変数(schematic variable)またはアンノウン(unknown)といいます。スキーマ変数は論理的には自由変数と同じですが、Isabelleの証明では自由変数とは異なり他の項に置き換えることができます。 証明を終えるとその定理に含まれる自由変数がスキーマ変数に置き換えられることがわかります。これにより、新たな定理を他の定理の証明に使うことができるのです。実際に証明をしてみると、なんとなくわかってくるかと思います。ただし、スキーマ変数を意識する必要はあまりないでしょう。 1.5 Interaction and Interfaces Isabelleとshellで直接対話することもで
Isabelle Tutorial その1 - caeruiro
1. The Basics 1.1 Introduction Isabelleは汎用的な証明支援器であり、高階論理に特化させたものがIsabelle/HOLです。私は数学屋さんではないので、高階論理って何？とかは深く考えず進みます。 1.2 Theories Isabelleを使用して理論を構築していきます。理論とは、型、関数、定理の集まりです。理論Tを定義するには次のように書きます。 theory T imports B1, ..., Bn begin 宣言、定義、証明などなど end B1, ..., Bnは既存の理論で、Tをこれらの上に構築していきます。オブジェクト指向プログラムのクラスの継承みないなものです。名前が衝突する場合は、T.fやB.fなどと書いて回避します。ファイル名はT.thyとします。 既存の理論ファイルは次のページで探すことができますし、Isabelleをインストー
OCamlを使ったシステム開発まとめ - osiire’s blog
うちの会社(有限会社ITプランニング）でやってきたOCamlを使ったシステム開発の概要を書いておきます。ふと思うと今までまとめて公開したことはなかったなと。別に隠す程のものじゃないし、もしこれからOCamlを使ったプロジェクトを始めてみたい人の参考になれば嬉しいです。 2006年 某証券会社のWebサービスの一部を担当 株価を解析して、その結果をWebAPIとして提供。OCaml + MySQL。HTTPベースで提供されるXMLファイルが生データだったので、この時初めてXMLのパースにxml-lightを使った。これはかなり便利。その後も使い続けている。nc(network cat)ライクなモジュールも作った。行列変換のためにC言語との連携もしたけど、特に問題なし。そういえば、この頃はmarshalingが好きで、DBへmarshalingデータをそのまま保存して「Objectデータベース
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
TATSUNO Yasuhiro on Twitter: "Javaのジェネリクス完全に理解した"
S (ﾂｲｰﾄはｽﾚｯﾄﾞ全体をご確認ください) on Twitter: "@yoshihiro503 Wikipedia等では議論のある用語ですけど、私の知る限り研究コミュニティでは「型検査が成功したら、stuck状態にならない」のが「強い型付け」(strong typing)だと思います"
もりぐち！！！！