サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
iPhone 16
www.itpl.co.jp
オープンソースと関数型言語による プログラム解析と カバレッジテスト自動実行 有限会社ITプランニング 今井 敬吾 1 第12回組み込みシステム技術に関するサマーワークショップ @ ホテル日航豊橋 テスト手法 2つのアプローチ ブラックボックステスト プログラムの入出力に着目 尺度:「外部仕様通りに入出力される」こと ホワイトボックステスト プログラムの内部構造に着目 尺度:「プログラムの全部を通る」こと e.g. 命令カバレッジ、分岐カバレッジ、パスカバレッジ 課題: 自動化によるコスト低減 網羅性の向上 2 テストケースの自動生成問題 ブラックボックステスト: ○比較的平易に実装可能 外部仕様をツール入力可能な形で準備する必要あり ホワイトボックステスト: ○ソースコードから生成可能 高度なプログラム解析技術が必要 数学的に自動生成困難な場合も (eg. ハッシュ関数) 最近のツール
2012 9 1 Copyright© 2011 IT Planning,Inc All rights reserved. A B C A A B C ON (* 4 ON/OFF . *) let overwrite_mode = ref false let bar_graph = ref true let line_graph = ref false let scatter_diagram = ref false (OCaml) ( ) ON ON OFF OFF ON OFF ON OFF ON ON OFF OFF ON [ ON] ON[ OFF] let on_bargraph_click () = (* *) if !overwrite_mode then bar_graph := not !bar_graph (* *) else if !bar_graph then (
2012 3 5 Copyright© 2011 IT Planning,Inc All rights reserved. LEXIFI 2000 LexiFi DSL LexiFi Web ( ) 2006 Haskell/Microsoft F# 2002 Jane Stree Capital High-Frequency) OCaml 200 (private fund) Ruby on Rails Scala Xen Citrix Xen OCaml http://cufp.org/ Microsoft F# Web fpish.net 2011 Scala, Akka Scala, Akka, Play IntelliFactory ( ) TypeSafe ( ) yesod (Haskell) Web COBOL Haskell Lift (Scala) Web Pytho
2012-02-03 ネタ記録庫/Scala/Lazy型 ネタ記録庫/Scala/Android/sbt-0.11.2 ネタ記録庫/Scala/Android/sbt-0.10 ocaml-android 2011-12-27 ネタ記録庫/Scala/Android/Android SDKとエミュレータのインストール 2011-12-09 ネタ記録庫/OCaml RecentDeleted ProofCafe 2011-12-06 ocaml-nagoya 2011-10-09 ネタ記録庫/Scala/dispatch 2011-09-29 ネタ記録庫/SML/SML#のインストール 2011-09-28 ネタ記録庫/SML/SMLNJのインストール ネタ記録庫/SML 2011-09-12 ネタ記録庫/Scala/Android/NFC 2011-09-09 ネタ記録庫/Scala/An
CONGAとは? CONGA はWebページ埋め込み型のFXチャートです。 スクロールは信じられないくらい高速 かつ スムーズで、 スマートフォン を含む 主要なWebブラウザ に対応しています。 最新の CSS3 アニメーションを応用しており、Webブラウザの真の力とリッチなユーザ体験を演出します. サンプル 次のサンプルを自由にスクロールしてください。 CONGA のパワーを体験できます (Internet Explorerを除く, 後述)。
CONGA - CSS3-Optimized forex chart of NaGoyA provided by IT Planning Inc. at Nagoya, Japan What is CONGA? CONGA is a lightweight Forex-chart in a webpage. Its scrolling is incredibly fast and smooth, and supported on major web browsers including Smartphones . CONGA applies brand-new CSS3 animation effects, which will bring out the real power of web browsers and richer user experience.
2011-05-13 ocaml-android 2011-03-29 ocaml-nagoya 2011-02-03 ocamljsメモ 2011-02-01 OCamlテクニック/再帰型(Equi-recursive) 2011-01-01 camlp5 C共有ライブラリの作成 2010-12-23 活動記録/20080529 2010-12-02 ProofCafe ProofCafe/Coq01 2010-10-07 ProofCafe/ProofGeneral 2010-05-22 ProofCafe/crush 2010-05-21 Fsharp 2010-04-25 ProofCafe01 2010-04-22 論文読み会 2010-04-16 ネタ記録庫/OCaml 2010-04-06 ProofCafe/Coq02 2009-12-15 発表資料 2009-08-10
プログラム定理証明 弊社での、プログラム定理証明を用いたソフトウェア品質保証の取り組みについて紹介します。 iZE Smart Desktopミドルウェアの正しさ検証 (ソフトウェア科学会PPL2010においてポスター発表、TPP10にて発表) (有)ITプランニングは(株)アイズの「スマートデスクトップ・クライアント」の一部モジュールを請負開発し,その際証明支援器Coqを使用した. 本プロジェクトではD-Busで扱うデータとJSONとの相互変換に関して静的検証を行った. 具体的には,検証対象とする関数をCoqで定義した上で諸性質を証明し,Extract機能により全体のOCamlのプログラムと協調させるという方法を用いた. 今回行った検証の詳細と,実際にCoqを開発現場で使う上で行った工夫などを報告する. (PPL2010予稿集より) プログラム定理証明って? プログラム定理証明は、プログ
2010-12-23 活動記録/20080529 2010-12-18 ocamljsメモ ocaml-android 2010-12-07 C共有ライブラリの作成 2010-12-02 ProofCafe ProofCafe/Coq01 2010-10-07 ProofCafe/ProofGeneral 2010-09-02 ocaml-nagoya 2010-05-22 ProofCafe/crush 2010-05-21 Fsharp 2010-04-25 ProofCafe01 2010-04-22 論文読み会 2010-04-16 ネタ記録庫/OCaml 2010-04-06 ProofCafe/Coq02 2009-12-15 発表資料 2009-08-10 starterkit 2009-08-01 活動記録/20080331 RecentDeleted OCamlテクニック
2010-10-07 ProofCafe/ProofGeneral 2010-09-02 ocaml-nagoya 2010-05-22 ProofCafe/crush 2010-05-21 Fsharp 2010-05-19 ProofCafe 2010-04-25 ProofCafe01 ProofCafe/Coq01 2010-04-22 論文読み会 2010-04-16 ネタ記録庫/OCaml 2010-04-06 ProofCafe/Coq02 2009-12-15 発表資料 2009-12-08 活動記録/20080529 2009-08-10 starterkit 2009-08-01 活動記録/20080331 RecentDeleted OCamlテクニック/daemon 2009-06-05 活動記録/第11回 2009-03-25 活動記録/20080418 活動記録
何ができるの? † 大域脱出 例外処理 非決定性 wiliki:amb 例えば、 (let ((i (amb 4 6 7)) (j (amb 5 8 11))) (if (prime? (+ i j)) (list i j) (amb))) ;Value 23: (6 5) のようにすると '(4 6 7) と '(5 8 11) のうちから二つの数の和が素数になる組の1つを返します。 これを理解するのに、自分は3ヶ月かかりました。 ambは、バックトラック演算子です。動きを大雑把に言うと、 (let (i (amb 4 6 7))で、 i に 4 が入ると同時に、 この時点のツヅキ、 "6 7)) (j (amb 5 8 11))) (if (prime? (+ i j)) (list i j) (amb)))" を取り出して、スタックにpush。 次の行、 (j (amb 5 8 1
限定継続とは? † 継続は「その後の計算」を表現したものです。対して、限定継続は「特定の範囲のその後の計算」を表現したものです。つまり、継続がグローバルな「その後」とイメージするならば、ローカルな継続が限定継続という感じです。 限定継続を扱う演算子には主にshift/resetのペアとprompt/controlのペアがあります。それぞれ静的な演算子、動的な動的な演算子と呼ばれます。(その理由はschmeとかのdynamic bindingとかと関係あるらしいけど、よくわかりません)
OCamlではCMLスタイルのスレッド間通信が可能です。 Eventモジュールには基本的なイベント型やその同期関数が揃っています。 ところが、ivarやmvarといった共有変数が無い為に苦しい状況になっています。 例えばとても単純に、整数を渡して計算結果を(今回は倍にして)返してくれるスレッドを作ってみましょう。 すぐに思いつくのは、次のようなコードです。 let start_server () = let in_ch, out_ch = new_channel (), new_channel () in let rec loop () = let x = sync (receive in_ch) in loop (sync (send out_ch (x * 2))) in ignore (Thread.create loop ()); in_ch, out_ch let calc (i
クライアントを書く † Hello_client.mlを新規作成して内容はこうする。 open Thrift;; open Hello_types;; let s = new TSocket.t "localhost" 9090;; let p = new TBinaryProtocol.t s;; let c = new Hello.client p p;; s#opn; print_string (c#hello "Gemma"); print_char '\n'; s#close; ↑ クライアントをコンパイルする † Makefileを使うべし。 SOURCES = ./gen-ocaml/hello_types.ml ./gen-ocaml/hello_consts.ml ./gen-ocaml/Hello.ml Hello_client.ml RESULT = test_cli
継続とは? † まず、大域脱出の例を見てみましょう。 SEND+MORE=MONEY でも、 return"ラベル"を定義して、 (return (list S E N D '+ M O R E '= M O N E Y)) なんてことをやっています。 リストlisと述語手続きpredを取り、lisの各要素に順にpredを適用して、 predが真の値を返したら直ちにその要素を返すような関数findはこう書きます。 (define (find pred lis) (call/cc (lambda (return) (for-each (lambda (elt) (if (pred elt) (return elt))) lis) #f))) lambda (return) はちょっと奇妙です。 私は脳内で、 (define (find pred lis) (let/cc return (fo
次回の予定 † 日時:2008/09/24(水) 18:30〜 (開始時刻が変更されました) 場所:名古屋大学 IB館 南棟 5階 エレベーターホール 内容 はてなインターン中の講義内容紹介(Gemmaさん) javascript, NekoVM, swf, PHPにコンパイルできるocaml製言語haXeについて。(話者:?) ↑ [NEWS] † オープンソースカンファレンス2008 名古屋で発表してきました。 詳しくはこちら OCaml-3.10.2 来ました!(2008-02-29) http://caml.inria.fr/ocaml/release.en.html 3.10.1 からの変更点 主に不具合修正. windows環境下でstr.mliが見付からなかったら、再インストールしましょう。 OCaml-3.10.1 来ました!(2008-01-11) 3.10.0 からの変
Ocsigen † OCamlによる継続ベースWeb開発フレームワーク [#ud483357] 今井さんが試しています。 論文 Typing web interaction with Objective Caml 特徴 継続ベースWebプログラミング XHTMLの静的チェック セッションの自動管理 モジュール指向 HTTPサーバの実装には協調スレッドを利用。 カウンタはこう書けます。 let compt = let next = let c = ref 0 in (fun () -> c := !c + 1; !c) in register_new_service ~url:["compt"] ~get_params:unit (fun _ () () -> return (html (head (title (pcdata "counter")) []) (body [p [pcda
次回の予定 † 日時:2008/10/22(水) 18:30〜 場所:名古屋大学 IB館 南棟 5階 562室 (あいていれば) 内容 javascript, NekoVM, swf, PHPにコンパイルできるocaml製言語haXe? コンパイラのコードリーディング (小笠原さんがいらっしゃれば) type improvement について ↑ [NEWS] † オープンソースカンファレンス2008 名古屋で発表してきました。 詳しくはこちら OCaml-3.10.2 来ました!(2008-02-29) http://caml.inria.fr/ocaml/release.en.html 3.10.1 からの変更点 主に不具合修正. windows環境下でstr.mliが見付からなかったら、再インストールしましょう。 OCaml-3.10.1 来ました!(2008-01-11) 3.10
while true do let line = read_line () in print_string line done
Copyright (C) 2006-2007 IT Planning Inc. All Rights Reserved.
このページを最初にブックマークしてみませんか?
『有限会社ITプランニング(IT Planning Inc.)』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く