猫行天下 摄影·生活

这两天在折腾着看Java PathFinder[Havelund, NASA Ames Research Center, 2000]。说实话Java的课程没有选修，所以对Java本身几乎一无所知。稍微深入一点点的了解来自编译课上介绍javac生成bytecode，其实一点也不深入，仅仅是提到而已。以下援引Klaus Havelund的Model Checking Java Programs Using Java PathFinder中的摘要部分：

This paper describes a translator called Java PathFinder (Jpf), which translates from Java to Promela, the modeling language of the Spin model checker. Jpf translates a given Java program into a Promela model, which then can be model checked using Spin. The Java program may contain assertions, which are translated into similar assertions in the Promela model. The Spin model checker will then look for deadlocks and violations of any stated assertions. Jpf generates a Promela model with the same state space characteristics as the Java program. Hence, the Java program must have a finite and tractable state space. This work should be seen in a broader attempt to make formal methods applicable within NASA’s areas such as space, aviation, and robotics. The work is a continuation of an effort to formally analyze, using Spin, a multi-threaded operating system for the Deep-Space 1 space craft, and of previous work in applying existing model checkers and theorem provers to real applications.

JPF属于模型验证技术中的模型检测（Model Checking）。其本质是构造DFA遍历有穷状态空间，检查系统的模型是否满足给定性质，例如在并发系统中发现死锁（Deadlock）和竞争条件（Race Condition）。含糊点说，JPF本身就是JVM，通过显式的遍历bytecode中所有可能的执行路径，发现各种错误。

模型检测方法带来的一个总所周知的问题就是状态爆炸。即让DFA变得不再那么“确定”（definite）/______\ 接下来更深入的内容还在阅读中。

—————————=”=—————————————–

看到pathfinder这个词会有怎样的联想，寻路者？或许吧。很深刻的一个词。

今天昨天到朋友家吃饭，本以为来回耗时3小时，结果单程就把留给路上的时间全耗完了= = 说起这两个朋友很是神奇，他俩因为某种很神奇的机缘巧合认识了，更神奇的是他们相恋了，并以惊人的速度进展着，其中一人从大连搬来北京，最神奇的是他们今天告诉我，他俩明年就要结婚了。生活就是这么奇妙，就在10来个月前他们还只是刚刚认识，偶尔一起打打游戏的两个人，如今满脸幸福的宣告结婚计划。就像去年的糖糖，忽然一个电话过来说她结婚了，然后闪电飞到米国去不回来了。一切的发展总比你能想到的要快。

这就是生活中的状态爆炸。每个pathfinder都期望在这个复杂系统中找到一条能让自己更舒服的path。

今天和那两人聊了很久，生活爱情婚姻家庭。最近，不对，是一直热衷于窥视不同的人在不同环境不同时期下的生存，状态也好信念也好，每个人的生活都是一本读不完的书，我只是抓紧机会多读几本多读几页。虽说戏谑之词穿插于对话当中，但他俩给人格外稳重成熟的感觉，大凡谈婚论嫁时估计都是这样吧。谈他们甜蜜的日子，北京房价，怎么过活，女人的需要，男人怎样疼女人，原则问题……很多一个人想不通的问题，三言两语的玩笑之间竟能看出一点真理来。看着他们俩平静幸福的样子，我心里倒也不知为何有种踏实。他们算是找到自己的路了，并会相互搀扶着一起走下去，祝他们幸福。

i’ ll be a pathfinder in peaceful pace.

近日翻照片，找到昔日小妾（本本是正室。。虽说如今状况又不一样了= =）的玉照，也是它属于我的日子里最后的照片。

Casio PX-400R，是从一个音乐学校的学生手上买来的，成色很漂亮3.5k，功能非常强大，特别是自动伴奏算是casio飘韵系列中最强大的。其实它的很多功能我都没有用到过，键盘左边有一个歪音轮，是为那些做midi的人设计的强力工具，到我这儿倒成为一个无聊时的好玩具，听着扭曲的声音很有快感。

森海塞尔HD497也是为了练琴而买的，同样也是二手的， 不过用着很舒服（在本学期惨遭室友蹂躏后有一边不好使了。。）。据寝室那帮阿宅们说，我练琴就是在敲鼓，虽说带了耳机，但是重锤的声音更让人心烦= =，唉 跟这帮没爱的家伙没有共同语言。

一年前为了买相机，不得已把爱琴贱价出售了，成为至今一大憾事。但是也没办法，不卖琴就买不了相机，相机与钢琴不可兼得。记得一个人待在寝室只有它陪伴的日日夜夜，记得第一次用它为班上的合唱伴奏，记得第一次见到它，记得最后一次弹起它……

忽然很想练琴。想到的是のだめ听了千秋弹拉赫玛尼诺夫以后吼的那一句：ピアノを弾かなきゃ！