■ - ひとり勉強会
ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。 金曜日は YARV: Yet Another Ruby VM のソースコード読みの日です。 履歴 (1): main から yarv コアに到達するまで (2): コンパイル処理の流れとデータ構造 (3): if のコンパイル (4): case, while のコンパイル (5): break, next, redo, retry, rescue, ensure, for, ブロック のコンパイル (6): 代入 のコンパイル (7): 自己代入, メソッド呼び出し のコンパイル (8): super, yield, リテラルなどなど のコンパイル (9): def, class, module, alias などなど のコンパイル ここまでのまとめ: PPT or PDF (10): 最適化 (11): バイトコー
YARV: Yet Another Ruby VM
What's new? What's this? DownloadLatest revision 0.4.1 Old tarballs HEAD License How to install?Requirement Build and Install run benchmarksrun all benchmarks run a specific benchmark YARV Benchmark for each options Documentation and ReferenceWiki Bug Tracking System (BTS) Common in English in Japanese ContactMailing ListEnglish (yarv-dev-en) Japanese (yarv-dev) YARV commit mail IRC Channel Mail a
ひとり勉強会
VSTTEという国際会議の開催した「ソフトウェア検証大会」 https://sites.google.com/site/vstte2012/compet 問題文PDF に挑戦していました。48時間で5問の仕様と実装が提示されて、その正しさ、つまり停止性や、配列の範囲外アクセスをしないこと、仕様を満たしていることなどを、なんでも自由なツールを使っていいから検証してみよう！というコンテストです。 というわけで、Coq でやってみて、力尽きました。難しいですね！コードだけ貼り付けておきます（提出はしてない）。 Problem 1 とある bool のソートアルゴリズム。 Coq で書けたので停止性は示されているはず 配列は範囲内であることが証明されている整数でしかアクセスできない依存型なのでアクセスも安全なはず 返値が sorted であることも証明付きの依存型なので大丈夫なはず 元のpermu
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
