RustのREPL "evcxr" を使ってみた - 簡潔なQ
概要 evcxrはRustのパーサーとコンパイラを外部から呼び出すことでREPLを実現している。セミブラックボックス的なアプローチにも関わらずなかなかの完成度で、今後が期待できる。 evcxr evcxrは最近公開されたRustのREPL (GitHub, redditのpos)である。また、Jupyterのカーネルもあるため、Jupyter Notebook上でRustを書くこともできる。 Evaluation Context for Rust とのことで、 ev + cx + r と思えば覚えられる。 インストール方法 コマンドラインは以下で入る。 cargo install evcxr_repl Jupyter版については公式サイトを参照するとよい。 基本的な動作を試してみる。 $ evcxr Welcome to evcxr. For help, type :help >> :he
Rustの型推論の概略 - 簡潔なQ
概要: Rustの型推論の大枠を説明する。 なお、筆者もRustの型推論の動作を詳細に把握しているわけではない。 短くまとめると Rustの型推論はHindley-Milner型推論ベースである。したがって後方の式や文の内容から手前の型が推論されることもある。しかし以下に挙げるようなRust独自の特徴をもつ。 型推論は原則として関数定義の中で閉じており、関数の引数型や戻り値型は推論されない。これは、関数を抽象化の境界とするための意図的なものである。この意味で「局所的」というのであれば間違いではない。 ただし、let多相を含む型推論を避ける意図もあるかもしれない。 関数呼び出しや一部の演算子などは、その部分の制約を立てる段階で、型の一部分が判明している必要がある。この動作は推論順序の影響を受ける。 トレイトによりオーバーロード可能になっている関数や演算子は、射影型を使っている場合、ボトムアッ
Rustのパニック機構 - 簡潔なQ
概要: Rustのパニック機構は異常終了の処理を安全に行うためにある。この動作を詳しくみていく。 パニックとは何か Rustには2つの異なる例外処理機構があります。 発生源 対処方法 例 パニック プログラミングエラー 原則として捕捉しない assert!() 境界外参照 Result 例外的な入力 必要に応じて捕捉 I/Oエラー (File::read) パースエラー (str::parse) パニックとResultの関係についてはTRPL第2版第9章、未定義動作とパニックの関係についてはRustonomiconのUnwindingの章などが参考になります。 パニックを想定した安全性 Rustではたとえパニック状態でも未定義動作だけは絶対に避ける必要があります。そのため以下の関数は不健全 (unsound)です。 use std::ptr; // この関数はRustではunsound (
末尾再帰をループにできないRustプログラムの例 - 簡潔なQ
概要: 生存期間の関係で、ループでは書けないが末尾再帰では書けるアルゴリズムの例を挙げる。 単方向リンクリスト 次のような単純なリンクリストを考える。 struct List<T> { root: Option<Box<Node<T>>>, } struct Node<T> { value: T, next: Option<Box<Node<T>>>, } backの実装 単方向リンクリストの末尾要素の取得は O(n) である。これは次のように書くことができる。 impl<T> List<T> { fn back(&self) -> Option<&T> { let mut node = if let Some(ref b) = self.root { b.as_ref() } else { return None; }; while let Some(ref b) = node.next
C/C++の静的解析ツール・事例まとめ - 簡潔なQ
C/C++の静的解析は、どう考えても大変なんだけどどう考えても需要が高いので、やはり色々なソフトウェアや事例があるようだ。まとまった情報が欲しいけど見つからなかったので自分の調べた範囲でまとめることにした。 他にも耳寄りな情報があったら教えてほしい。 静的解析を行うことができるソフトウェア 調べてみると結構たくさんある。それぞれの特徴とかあまりよくわからない。 (個人的には、とりわけ網羅的な形式的検証ができるツールの性能に興味があるので、それを中心に集めていたが、やはり網羅的とは限らないで探すともっとたくさん見つかるようだ。もちろん網羅性にはトレードオフがある) Frama-C …… C言語に形式手法を適用するための汎用のフレームワークで、静的検証のためのプラグインも多数(WPとかValueとか)存在する。網羅的な検証から発見的な手法、動的な手法まで様々ある。研究で使うのに便利そう Ast
CoqのtacticをOCamlで書く話 - 簡潔なQ
CoqのtacticをOCamlで書いてみたので、同じようなことをしたい人のためにメモ。 なお私はOCamlについてはそれほど詳しくないので、そこの正確性については注意が必要。 同じ事をしているtacticがないか探す 同じようなことを考えている人は必ずいるはず。といっても、網羅的な探し方があるわけではないので、ある程度調べて見つからなかったら自分で書いたほうが効率が良いかもしれない。 まずCoq自体にないかを調べる。Coqの基本的なtacticsは Tactics Indexに書かれている。 Coqのcontribution集に似たような内容のものがないかを調べる。contributionは の「All contribs」というリンクから一覧できる。 特に、AACTacticsは有用らしく、Ubuntuのパッケージにもなっているようだ。 ssreflectには有用なtactic/tact
Cプリプロセッサメタプログラミングで、文字列系泥沼関数型プログラミング - 簡潔なQ
今年の文化祭で書いた記事です。 - C言語といえば、いやなイメージ、過去の遺産といった感じがあるかもしれません。 C言語のネガティブな側面というと、やはりポインタやメモリ管理などが難しい、ということが思いつくかもしれません。 しかし、C言語のポインタは表記に騙されやすいだけで、仕組み自体は全く難しくありません。 文法も、どこぞのPerlやC++と比べたら屁でもない単純さです。 実のところ、仕様が煩雑で難しいのは、Cプリプロセッサなのであります。 普段からあまり複雑な使いかたをしないから気づかないかもしれませんが、Cプリプロセッサの置換処理は、欺瞞と裏切りに満ちた世界なのです。 これが進化するとテンプレートなどといったもっと面白いものになるのですが、今回はCプリプロセッサで計算をしちゃったりするところまで試しにやってみましょう。 (なお、GCCにより実験的に調べた記事なので、他のCコンパイラ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
