Prustiを使ってRustでプログラム検証をしよう導入に際し、ドキュメントに書いてないこととか色々あってつらかったため、軽くメモ代わりに投稿しておきます。 また、Prusti を使う最も簡単な方法は VSCode の拡張である Prusti-Assistant を使うことですが、Vimの使用を見越しコマンドだけで使えるようにアレコレ設定しました。 Prusti の紹介 プログラミングにおいて、関数に対してプログラマが明示的に制約を課すことはよくあります。 例えば、次のような単純な関数 max を考えます。 fn max(x: i32, y: i32) -> i32 { let result = if x > y { x } else { y }; result } さて、この関数は次のような性質を持つことが期待されます。 resultはx以上かつy以上 resultはxまたはy そういった情報は多くの場合ライブラリのドキュメントなどに書い
