VDMでは、functionとoperationの使い分けって微妙です。 これ、Javaではどちらもメソッドにあたります。 どう使い分けするのかが悩みます。 しかも、文法が結構違うので、途中で簡単に変更できないのも厄介です。 そのため、最初にどちらで記述すべきかを決…

停止性の証明が有効なのは、functionだけですね。operationでは証明課題が生成されません。

「あんさん、スーチーさん？」 なぜかこのフレーズだけが、ぐるぐる回ってました。 ・・・寝不足です。