動機 現時点でRubyの最新版は2.4, サポートされているのは2.2までで、2.1以前はメンテナンス対象外である。そのような古いバージョンを動かすのは決してよいことではない。 しかし実のところ、現在でも多くのWindowsマシンで、Ruby1.8.1とRuby1.9.2p0が動作…

概要: Rust-proofはElectrolysisと同様にRustプログラムから検証条件を抽出するが、LeanではなくSMTソルバであるZ3向けの検証条件を出力する。こちらも開発が放棄されているように見えるが現在もビルド可能である。 準備 テスト用リポジトリを準備する $ car…

概要: ElectrolysisはRustの検証条件をLEANに出力するプロジェクトである。これを使ってみた。 Electrolysisとは Electrolysis (electrolysis: 電解) はSebastian Ullrich氏の修士研究で開発されたプロジェクトで、Rustプログラムの正当性や計算量に関する検…