サクサク読めて、アプリ限定の機能も多数!
トップへ戻る
ノーベル賞
eldesh.hatenablog.com
静的コード解析の会#6でVeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…) 前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。 が、今回の発表では多重集合、整礎関係、実際の処理系で検査できるコードについての説明まで入れることが出来たので、これで一通りの内容を盛り込めたと思います(ただしシーケンシャルなプログラムに限る…)。 参照している論文はModular termination verificationです。 (多分)怪しげな記述や展開のよく分からないページがありますが、がんばって作ったので興味がある人は是非眺めてみて下さい。 個人的なおすすめはStatic Recursionパターンの検証方法のあたり(資料の末尾の方)です。 会場からは、 処理系が(もっと)がんばれ 発表の構成が悪い(直接そうは言われてないけど) とい
静的コード解析の会#2でVeriFastによる停止性検証の導入の話をしてきました*1。 本当は私自身も発表するほど分かってないのですが、それでも楽しい部分はあるので「これまで理解している内容を詰め込んでみた」という感じでまとめてみました。(前日深夜から突貫だったので超眠かった…) 今回の発表で伝わったかは怪しいですが、停止性のために最低限の機能を導入し、既存の機能を活かした仕組みはとても素晴らしいと思います。 楽しい部分を端的に挙げると、 多重集合のある種の順序関係からどんどん「関数を呼ぶ権利」が出てくる 関数の順序関係をコード上の大小関係で決めた まぁこれだけ聞いても絶対分からないので、詳しく知りたい方はModular termination verificationを読みましょう。 振り返り 前回に引き続きVeriFastの話ですが、今回の内容は前回と比べて取っつきにくい内容でした。
C言語の静的自動検証器である Infer の使い方がある程度分かってきたので紹介します。 Infer Infer は、C言語(or [C++, Obj-C, Java])の検証器で、 自動で特定の種類のバグを発見してくれます。発見できるバグとして分かり易い例ではリソースリークを発見できます。 元々Inferを開発した会社をFacebookが買収してオープンソースになりました。(https://github.com/facebook/infer) スマートフォン向けアプリの検証に使っているようです。 追記: 勘違いしてましたが C++サポートはこれからのようです。> https://github.com/facebook/infer/issues/24 Separation Logic(分離論理) InferはSeparation logicという意味論に沿って静的検証を実行します。Sepa
2015/1/20現在、 これまで startxwin で使えていた、cygwinをXサーバにする方法が変更されて使えなくなった。ログから察するに2014/11/13の更新から。 新しい方法では以下のようにする。 $ run xwin -multiwindow $ xterm xterm> xhost +192.168.xxx.xxx (参考 X does not start after cygwin upgrade) 起動ログ 参考として起動ログ(/var/log/xwin/XWin.0.log)を張っておく。 Welcome to the XWin X Server Vendor: The Cygwin/X Project Release: 1.16.3.0 OS: CYGWIN_NT-6.1 user-PC 1.7.33-2(0.280/5/3) 2014-11-13 15:45 i
Github Pagesに使えそうなのでmanの該当箇所を訳してみました*1。=>原文 orphanブランチというのは、元のブランチからの歴史を受け継がず、gitリポジトリ内で新しく0から歴史を持つブランチです。新しくルートになり、親コミットを持ちません。 リポジトリの中から特定のファイルのみを公開したい場合などに使えそうです。 # 日本語として自然になるように努力はしてませんが、間違いは指摘していただければ直します Synopsis git checkout [-q] [-f] [-m] [[-b|-B|--orphan] ] [] Description Create a new orphan branch, named , started from and switch to it. The first commit made on this new branch will have
この記事は LL/ML Advent Calendar #LLAdventJP 20012/12/20の参加記事です。 出来心でRTした次の瞬間には犠牲に参加することになっていました。なごやこわい。 注意:この記事では SML#1.2.0 を使うものとしています。 SML# にはC言語バインディングをサポートする機構が言語レベルで組み込まれており、簡単にC言語で書かれたライブラリを利用することが出来ます。 しかしまぁ、簡単とは言っても相手はあのC言語ですよ。 現実世界のライブラリをバインドするにはキレイな世界だけで完結するはずも無いのです…。 ここでは、私がまともに使い始めて分かってきたことを含めて、基礎からSML#のC言語バインディングの機能を一通り紹介します。 いきなり例 もう界隈の人にはおなじみかもしれません。最も簡単なバインディングの例です。 # val puts = _impor
C++のにある numeric_limitsテンプレート は, 実装依存のarithmetic typeに関する性質を提供します. テンプレートとは言っても, 実装依存の値を一般化して求めるなんて出来ないので, (というかそれを提供するのが目的) それぞれの型についての特殊化を定義してあります. 使ってみる. #include <iostream> #include <limits> using std::cout; using std::endl; #define PRINT(expr) cout << #expr << ": " << (expr) << "\n" int main () { PRINT(std::numeric_limits<int>::min()); PRINT(std::numeric_limits<int>::max()); PRINT(std::numeric
BoostCon2011で発表されたBeman DawesさんによるProposed Boost B-tree Libraryを和訳しました! 翻訳した資料はslideshareに挙げました。 boostjpからも辿れます。boostjpには他の方の資料へのリンクも張られるはずですのでご期待ください。 Proposed boost b_tree_library(ja)View more presentations from Takayuki Goto. ご本人からも許可を頂いてます :) Yes, of course you may reprint the presentation translated into Japanese! Thanks for the interest,BtreeかわいいよBtree(*´д`*)
使いたいスクリプトが内部でcurlでファイルを落としたがってたけど, 基本的にプロキシを通さないと外に出れない場所に居たのでmanを見る. 全体の設定 ALL_PROXY [protocol://][:port] HTTPの設定 http_proxy [protocol://][:port] https HTTPS_PROXY [protocol://][:port] ftp # コメントを受けて修正@12/08/04 FTP_PROXY [protocol://][:port] ホワイトリスト(?) NO_PROXY …おわかりいただけただろうか!? HTTPの設定 http_proxy [protocol://][:port] httpのみ小文字じゃないと認識しないとかどんだけだよ!!!*1 *1:manにはしっかり小文字限定って書いてあるけど
ちょっと文章が直訳っぽくてところどころ不自然だけど,丁寧にBoost.MPLの実装(と使い方)について解説してあってとても分かり易い! 個人的な需要にぴったり合ってたこともあると思うけど,MPLの基本的なことを理解するにはかなり良い内容だと思います. ただ,表紙の宣伝文句(メタ言語としてのC++がマスターできる)というのはどうみても誇大広告w (勝手に汲み取った)対象読者 テンプレートの振る舞いが一通り分かる(気がする) ModernC++Designに洗脳された MPLを使いこなせているとは言えない なんという俺! 以下自分なりのダイジェスト. 前半 丁寧なBoost.MPLの解説. この前半の解説が分かり易かった. 書いてあることはMPLのリファレンスとほとんど同じ内容なので,それだけで分かる人はこの本要らないかも. メタ関数転送(継承するだけ) typedefする手間が減る ネストし
いわゆる Parallel ML の一つである MPL の論文最新作です > Efficient Parallel Functional Programming with Effects: Jatin Arora Sam Westrick Umut A. Acar. PLDI 2023. 重要な拡張に思えたので全体を読みましたのでメモしておきます。 MPL MPL はいわゆる Parallel ML の実装の一つで、(dis)entanglement という性質に基づいたメモリマネージャを搭載することで、コア数に沿って関数型並列プログラムの実行速度がスケールする(ことを目指している)SML処理系です。 並列化の方針としてはExplicitかつNested Parallelismです。 実装としては MLton をフォークしていますので、シーケンシャルプログラムの実行速度はひとまず十分であろ
このページを最初にブックマークしてみませんか?
『::Eldesh a b = LEFT a | RIGHT b』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く