やっと「エレベータ」の仕様をVDMで記述できました。 とりかかる前は、「たかがエレベータだろ?」と甘く見ていたのだけれど、やってみて、コレがとんでもなく難しく、奥が深いのに気づきました。さすが「形式手法の先生がた」が出しただけのことはあります…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。