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 の続き。 検証条件をいちいち人間が確認するのは面倒。 なので、検証条件の中に現れる変数に適当な値をぶち込んで、条件が成り立つかどうかを自動的に試せるようにした。以下は、検証条件の中に変数が３つあるので…

そうそう、この前、婆さんの法事で親戚が集まったとき、渡辺の「辺」の字の話題になったのです。普段はやさしい「辺」の字を使っていますが、正式には難しい方の字なのです。 （私の苗字は渡辺です） コンピュータでは「邊」という字がありますが、それとも…

実は前回のソースは動きません。 http://d.hatena.ne.jp/a-san/20060217#p1 言語側のバグがあって、Internal Errorを起こします。どひゃー！！！＼（＾ｏ＾）／ あれからメールで報告し、今日、何とかバグと認めてもらって、近日中には直るらしい。 まぁ、面…

あれっ？ まだ日本のメダルの数は０なのかー。 まぁ、国別に数えたって仕方ないけどね。 ここまで０なら、このまま０で終わってもいいんじゃない？

ロシア「ウラン、いらん？」 イラン「イラン、いらん！」 ロシア「ウラン、売らん！」 くだらね〜

を見つけたので、メールにて報告。 まぁ、初版ですから。 (追記)返事が返ってきました。平成16年12月10日 第1版第2刷では直っているらしいです。この本この前買ったばかりなのに〜

http://dontaku.csce.kyushu-u.ac.jp/books/ProgramSpecification/ IT Text プログラム仕様記述論 を見ながら、静的検証を行うプログラムを作ってみました。 プログラムと、事前条件＋事後条件＋ループ不変条件を設定すれば、検証条件を出力します。 言語体…

だいぶ文法がわかってきたので、簡単なクラスを作ってみました。 まったくの未開の大陸なので、すべてが手作りから始まります。 例えれば、すらないC言語です。まぁ、面白い半分、苦労も多々。 /** * 有理数のクラス * 分子、分母は整数である。 * 分母は０…

久しぶりにプールで泳いだら、しんどい、しんどい。 息はゼーゼー。心臓バクバク。 オマケに足がつっちゃった。ハハハ（笑）

JRootPane.setDefaultButton(JButton)を使います。 JFrame frame = ... JButton okButton = ... fraem.getRootPane().setDefaultButton(okButton); マイナーなクラスなので探すのに苦労しました。

http://d.hatena.ne.jp/a-san/20060208#p1 水が上がるのは、周りの水面の高さまでです。水が勢いよく後ろに出ることはありません。 マンガなどで噴水のように水が沸いていることがありますが、あんなことは起こりません。水の高さはせいぜい水面の高さまでで…

十字分割窓のひな形を作ってみました。 もうチョット丁寧に作らないとダメですが、基本的な動作はできてます。 import java.awt.*; import java.awt.event.*; import javax.swing.*; import javax.swing.border.*; import javax.swing.event.*; public class…

選択したテーブルの CREATE TABLE文を自動生成する機能をつけてます。 で、どんな書式で書くかが問題なのですが、テンプレートに従って出力するようにしました。 しかもテンプレートはXML形式です。カッコイイ！＜自画自賛（＾ｏ＾） 以前も似た機能を作った…

船に穴をあけ、パイプを通して後ろに向けると、人の重さで水が勢いよく後ろに出てきます。 そのため船は漕がなくてもゆっくり前に進むことができます。それに沈むこともありません。 本当にこのような船を作ることができるのでしょうか？ 答えはもちろん無理…

swing.plaf配下のクラス関係を確かめて、再度Swingソースへダイブ。 こんどはうまくいきました。ふぅ〜。 import java.awt.*; import javax.swing.*; public class RendererTest2 extends JPanel { JLabel renderer = new JLabel(); CellRendererPane render…

http://d.hatena.ne.jp/a-san/20060127#p2 再描画が無限に続くことが判明。ダメじゃん。 で、数時間、swingソースにダイブしたが結局わからず。 どうもSwingはL&Fの仕組みのせいでわかりづらい。 一つの収穫はjavax.swing.CellRendererPaneを見つけたこと。…

やっとオープンしました。早速ユーザ登録！ http://www.vdmtools.jp/ あぅ！このツール、古いバージョンじゃん。読めないprjファイルもそのまま。最初は誰もがexampleを触るし、その唯一のprjファイルが読めないんじゃ印象悪いです（Ｔ＿Ｔ）。特に今回は新…

JTableなどでおなじみのセル・エディタの尻尾をつかみました。 どうもSwingはL&Fの仕組みのせいでわかりづらい。 import java.awt.Rectangle; import java.awt.event.*; import javax.swing.*; /* セルエディタのひな形 * 作成日: 2006/02/01 */ public clas…