タグ

verifyとwhyに関するmasterqのブックマーク (2)

  • GitHub - creusot-rs/creusot: Creusot helps you prove your code is correct in an automated fashion.

    You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert

    GitHub - creusot-rs/creusot: Creusot helps you prove your code is correct in an automated fashion.
    masterq
    masterq 2022/11/15
    RustコードをWhy3に翻訳して検査する。事前事後条件とループ不変条件を書ける。量化子を使える。注釈で使う関数は停止する。Why3側でどの程度手動の証明が必要なのだろう?Prustiより検査が速いと主張している
  • 書いたコードが一発で動作するとなぜ不安なのか : akiyan.com

    書いたコードが一発で動作するとなぜ不安なのか 2013-04-21 プログラミングにおいて少なくないコードを一気に書き上げたとき、そのコードが一発で動作 or テストケースに通るとなんともいえない不安を覚えるのは、プログラマーなら誰でもあるあるネタだと思う。「当にこれ、一発で動作しちゃっていいの? 俺、そこまでミスしないプログラマーだっけ?」なんて自分を疑ったりする。 このあいだもそんなことがあったんだけど、ふと気になった。不安になる理由は、自信のなさからくるものだけだろうか? ちなみに、書いたコードが正しく動作しないとき、コードを修正すると不安になることはない。一体、なぜ? 一発で動作したブラウザの画面を見ながら、考えてみて、閃いた。「コードの修正は、書いたコードを見直す機会にもなっているから」じゃないだろうか。コードの見直しは「リファクタリング」といっていもいい。 一発で動作してしま

    書いたコードが一発で動作するとなぜ不安なのか : akiyan.com
    masterq
    masterq 2017/02/26
    そこで静的検証ですよ!
  • 1