p260-2001fpのブックマーク - はてなブックマーク

C言語によるCBMC(有界モデル検査技術)を使用したPDD(証明駆動開発) - ジャンク☆ニュース臥龍
C言語によるCBMC(有界モデル検査技術)を使用したPDD(証明駆動開発)を藤倉さんが提唱されている。 http://tfujikura.blogspot.com/search/label/PDD OCaml似の文法を使用するCoqによる証明駆動開発に比べて、c(c++)言語で仕様を書けるのでとてもわかりやすいと思う。 http://d.hatena.ne.jp/garyo/20110301 CBMC-PDDについて色々調べてみたいです。 CBMC (Bounded Model Checking for C/C++)は以下でWindows版、Linux版などがダウンロードできます。 http://www.cprover.org/cbmc/ 簡単な使い方は島さんのブログがわかりやすいです。 http://saltheads.blog134.fc2.com/blog-entry-1.html
p260-2001fp 2011/05/06
開発

CBMC

PDD
リンク
C言語による組み込みTDDまとめ - ジャンク☆ニュース臥龍
C言語でTDDを行う場合、また組込み系でTDDを行う場合、色々問題が発生する。スタブ関数名の競合クロスコンパイル環境(実機の容量不足、実機用CPUで使えるツールが少ない(カバレッジ計測など)）グローバル変数の使い過ぎで単体テスト不可私の場合は以下のようにして行った。 1.関数のモジュール仕様書を作成し、関数名、関数毎の引数、戻り値を定義 2.上記よりスケルトンを作成(自動) 3.ターゲットCPU依存のデバイスをパソコン用にスタブ関数とヘッダーを作成 (擬似FROMのR/W,SIOのR/W,ポートのI/Oなど) 4.Cygwin上でCUnit for Ando でスケルトン用にUnitテストを実装 5.単体テスト実行後、スタブを実機用のドライバーに切り替え（ヘッダーファイルを変更）実機に組み込み。 C言語におけるTDDの問題点と解決方法組込み開発におけるテスト駆動開発事例〜C言語
p260-2001fp 2011/03/02
組込み開発でTDDを行う手法。ハード依存部分をスタブに置き換えてPC上で単体テスト。やはり行き着く先はこの形になるようだ。シミュレータ等の導入は難しい

TDD

BDD

組み込み

開発
リンク
電卓に強くなる―すぐに役立つ公式と実例 - ジャンク☆ニュース臥龍
昔電卓に強くなる―すぐに役立つ公式と実例ブルーバックス (B327) という本を読んで、色々公式覚えて、普通の電卓でlogやln,sin,cosを出して遊んでいた。普通電卓があったので、思い出そうとしてみてもlogの公式しか出てこなかった。これはlogを出したい値を入れておいて（例「２」）「√√√√√√√√+1/=2=-1*222.36」でlogが出てくると言うもの例えば２で計算すると 2√√√√√√√√+1/=2=-1*222.36 は　0.3010309になる。関数電卓だと　0.30102999566398119521373889472449　なのでほとんどあっている。三角関数の公式もあったけど思い出せない。高校数学の対数表のコピーを下敷きに入れて、物理の計算で使ったりしていた。元の近似式の記事があった。気賀さんの近似公式は侮れません、、、丁寧に作成されたのがわ
p260-2001fp 2010/05/20
リンク
1