kencoba https://blog.hatena.ne.jp/kencoba/ kencobaの日記 https://kencoba.hatenadiary.org/ VDM http://topse.or.jp/docs/?q=node/16 受けてきた。VDM++のイントロダクションとして良い勉強になった。 実際使ってみると、陽定義で操作の中身を書くのは簡単。 難しいのは事前条件、事後条件を抜けもれなく書くことだ。以下は演習課題の一部分 -- multiChoose public multiChoose : set of UserID * nat ==> set of UserID multiChoose(users,num) == ( dcl res : set of UserID := {}; for i = 1 to num do ( let x in s… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fkencoba.hatenadiary.org%2Fentry%2F20110126%2F1296007115" title="トップエスイーチュートリアル「VDM++による形式仕様記述」 - kencobaの日記" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2011-01-26 10:58:35 rich https://kencoba.hatenadiary.org/entry/20110126/1296007115 1.0 100%