C言語によるCBMC(有界モデル検査技術)を使用したPDD(証明駆動開発)を藤倉さんが提唱されている。 http://tfujikura.blogspot.com/search/label/PDD OCaml似の文法を使用するCoqによる証明駆動開発に比べて、c(c++)言語で仕様を書けるのでとてもわかりやすい…

ほむら「佐倉杏子には本当に美樹さやかを救える望みがあったの？」 キュゥべえ「まさか。そんなの不可能に決まってるじゃないか」 ほむら「ならどうしてあの子を止めなかったの？」 キュゥべえ「もちろん無駄な犠牲だったらとめただろうさ」 キュゥべえ「で…