http://ysserve.int-univ.com/Lecture/SetTheory3/settheory01/node1.html 集合の基礎的性質その１http://krakatoa.lri.fr/ The Krakatoa Tool for Java Program Verificationhttp://pvs.csl.sri.com/index.shtml PVS Specification and Verification System

http://www.cs.iastate.edu/~leavens/JML/index.shtml 形式手法のノウハウをJavaに生かせないか考えていたんだけれど、すでにこういうのがあった。どうやら、javadocみたいにコメントに事前条件、事後条件、不変条件などを書くみたい。静的検証ではなく動的…

http://d.hatena.ne.jp/a-san/20060219#p1 の続き。 検証条件をいちいち人間が確認するのは面倒。 なので、検証条件の中に現れる変数に適当な値をぶち込んで、条件が成り立つかどうかを自動的に試せるようにした。以下は、検証条件の中に変数が３つあるので…