赵翔鹏的Blog Xiangpeng's Thinkpad

在痛苦中感悟 — My Path of Renaissance

今天又翻了一遍以前的日志。其实来澳门的前半年内，我都处于很低落的状态，大部分时间都过得比较痛苦。还好，现在基本上已经坚持过来了。读着日志，几乎有点惊讶于自己的转变和成长。看着最近那么多博士自杀的新闻，更感觉人一定要想得开。

每个人的抗压能力、适应能力是不同的。问题是如何提高这些能力？根据我的个人经验，读一点哲学很有助于解决问题；同时朋友的帮助也非常关键。

每到一个新的环境，人总是会试图证明自己。如果自己没能达到心中给自己的定位和要求，不管你是个刚步入高等学府的大一学生还是个刚参加工作的博士后，总会
感到非常痛苦。而且，很不幸的是，根据管理学的原理，人最终总会被提升到一个他所不能胜任的位置上。所以我想，人要学会保持平常心。WZY兄的座右铭“永
远把艰辛的劳动当作是生命的必要，即使没有收获的指望也心平气和地继续耕作”说得很对。这句话我以前不懂，现在，似乎懂得一点了。

p.s. 以上文字是对前半年的反思，现在我的心情很好。:)

从“看布告”到“订报纸”：我对RSS和Bloglines的印象

以前的web1.0像宿舍楼下张贴的公告。我必需每天都凑到跟前去看一眼；而且这一眼看到的常常都是重复的信息——毕竟大多数时间都没有新的公告贴出来。最讨厌的是，如果不天天去看，就可能会错过重要的信息。

今天的rss就是送上门的报纸。不管订了多少份，都会自动送到我这里，而不是让我到处跑来跑去地看这个教务处的公告和那个楼长室的公告；不会担心错过，内容也不会跟昨天的重复。

Bloglines则更进一步：你可以知道你的报纸是否流行（有多少人也订阅了），也可以知道别人都订什么报纸，甚至可以根据你已订的报纸，给你推荐一些你可能会喜欢的别家报纸。

所以，有了rss.sina.com.cn，我就不用隔一段时间就去翻阅 news.sina.com.cn看看有没有新消息了。

Model-checking UML的工业应用

一篇好文：Model Checking & UML 實例。

"雖然測試也可能找到相同的錯誤或不一致情況，但是Model
Checking在OOA時就可以去驗證檢查，Testing則必須要到OOP之後有程式碼才能檢查，所以成本會比Model
Checking還要高(越晚修改，cost越高)，且Model
Checking主要是檢查規格上的錯誤，無法去驗證效能和壓力，而這些主要是測試所要確認的。"

early verification是形式化方法的核心思想。工业界终于也开始理解这一点了，也开始关注model checking的应用了。

形式化方法并不是一堆研究生才能看懂的数学公式，形式化方法也可以是很简单好用的，如model checking。

解释计算机体系结构的搞笑图片

图片来自http://www.xtrj.org/，这其实是个不错的网站，虽然界面土了一点。

深圳·印象：大楼、美术馆与高交会

在大巴车上向外张望，深圳城市建设的现代化程度让人非常惊讶。新兴城市就是不一样！不存在“旧城区”的概念，到处都是完美的绿化和非常有个性的高楼。说到
高楼，每个中国城市都爱好盖，但盖得有个性的就罕见了。别的不提，若把招商银行大厦放到任何一个城市，恐怕都会成为这个城市的标志性建筑。刚刚奠基的腾讯
大厦门口两根包得金灿灿的柱子也向人炫耀着深圳的经济水平。

周四逛了正在展出复制的敦煌壁画的关山月美术馆。有一点让我极度极度的ft：张大千先生的作品竟然放在侧面的小厅，等我发现的时候时间已然不够。说实话，
看完中间大厅，我对敦煌简直有些失望，感觉“不过如此”罢了。然而大千先生临摹的壁画却有着惊心动魄的魅力：那是一种让人站在画前心情澎湃，久久驻足而不
愿离去的魅力——记得上一次有这种感觉还是在西安碑林的时候。看到后半，我几乎在怀疑，是不是先生稍微加入了自己的画风，所以这些壁画才与大厅的作品如此
不同？然而看到文字简介，方知先生临摹壁画的态度之严谨，几乎可与抄写经书的虔诚僧侣相比——“绝不可掺入己意”。自然，对敦煌壁画的敬仰又深了几分。

后来又至深圳大学，大概走了一圈。他们的科技楼比清华主楼还豪华，设计也相当巧妙；他们的文科教室楼里全部装有空调……

周五的高交会才是我们来深圳的正经目的。也许是之前期望太高，我对高交会有些失望。先说IT展区：国外的厂商非常少；国内的展商也多是些无聊的公司。
IBM、M$、Apple是绝不会来这里浪费时间的；看到Oracle的牌子提起些兴趣，走近了一看，原来是Oracal Partners
Network...
虽然神舟电脑的展台搞得很花，不过我坚决敬而远之。当然也有些不错的公司，像Lenovo、Hitachi还是认真的来的。ThinkPad的
Tablet
PC真酷。SAP悄无声息之间已经是国内ERP市场占有率第一了。这个公司有前途。看来国内企业信息化的市场恐怕将来也会被国外公司蚕食，毕竟技术水平相
差太大了。还有，中国移动的宣传册简直太奢侈了，从没见过质量这么好的铜版纸。移动的政府、企业信息化也是做的有声有色，很多好想法，比如已经很普及的企业***。（Update: 我再次极度佩服blog.edu.cn的内容过滤，"彩 铃"两个字被自动变成了***）

走到显示器展区，高清电视还是挺有视觉刺激的。标清是DVD的画质，而高清是超越DVD的画质。感觉各大电视厂商、手机厂商都布置的挺好。希望新做的SCDMA标准能走好，虽然我一向对CDMA没兴趣。

省市、大学展区很一般，比如所谓的北京大学展区基本就是北大深圳研究生院的几个宣传台而已，虽然远远看去，展台还是古色古香挺有特色。最有趣的是德国巴伐利亚展区，虽然展区做的非常好，但他们恐
怕是最失落的人了：有个展商是PDFLib，做PDF第三方API的；有个展商iSO是做air traffic
control的……跟附近某省的“自动洗拖把机”一比，真有点幽默感。

生物、机械之类的不懂，不敢妄加评论了。走马观花下来，累的快不能动了；现在觉得有点遗憾，应该找几个展商好好聊聊，比如SAP，PDFLib等等。总
之，我觉得，国内的IT业也就是那个样子；但是制造业似乎很红火，可惜大多我都不懂。同行的Irshad估计也有些失望。他以为这么一个国际性的高交会上
会有不少外国人参加，至少展商应该提供英文的介绍……不过，对于深圳这座城市，他也跟我们一样大受刺激。

然而，回程时再仔细想想，深圳虽然很modern，却不像北京给人感觉那么亲切，也不像上海给人感觉那么精致。也许是移民城市的原因，太多现代化的东西放
在一起，除了“modern”之外，反而让人找不到适合用形容这个城市特色的词汇了。一个城市文化的沉淀，也许是需要上百年才能形成的。想来想去，还是北
京和上海给我的印象最好。

九月十日忆重阳

重阳节澳门休假一天。在家折腾论文到下午4点，然后去珠海。买了两本字帖，自己在一家超豪华的饭店吃了顿几乎完美的湘菜，如果不考虑价钱的话。本来想给家里打个电话，不过回宿舍时已经太晚了。没去登高。

btw，昨天FASE给我发email说他们收到了破纪录数目的abstract……继ASPDAC之后，又一次遇到了这种不幸事件。命苦啊……还有，明后两天去深圳。刚好跟FASE截稿日期碰在一起。总不能带着笔记本去吧！只好今天就投出去了。

Update:

下午玩了玩扫描仪，挺好～扫了两行铅笔写的字，然后拿photoshop乱处理一下，就成了下面的样子。（嗯，我又在浪费时间了。。。）

---

秋登兰山寄张五 　　孟浩然 　　北山白云里，隐者自怡悦。相望始登高，心随雁飞灭。 　　愁因薄暮起，兴是清秋发。时见归村人，沙行渡头歇。 　　天边树若荠，江畔洲如月。何当载酒来，共醉重阳节。 九月十日即事 　　李白 　　昨日登高罢，今朝再举觞。 　　菊花何太苦，遭此两重阳。 九月九日忆山东兄弟 　　王维 　　独在异乡为异客，每逢佳节倍思亲。 　　遥知兄弟登高处，遍插茱萸少一人。 九日齐山登高 　　杜牧 　　江涵秋影雁初飞，与客携壶上翠微。 　　尘世难逢开口笑，菊花须插满头归。 　　但将酩酊酬佳节，不作登临恨落晖。 　　古往今来只如此，牛山何必独沾衣。 重阳席上赋白菊 　　白居易 　　满园花菊郁金黄，中有孤丛色白霜。 　　还似今朝歌舞席，白头翁入少年场。

rCOS讲座笔记

rCOS = A Refinement Calculus for Object Systems

rCOS基于UTP(Unified Theory of Programming)，但并不是说需要UTP的全部知识才能理解rCOS。（还好……:P）

跟Component Calculus相比，rCOS层次稍微低一点，但是完全延续了component calculus的思想。

component跟class的区别：“对于component，我们知道的是requirements；对于class，我们知道的是body”。"A
component is like a beast in a cage."，因为我们都是要通过一个“界面”来交流，存在清晰的“边界”。

我总觉得这里的component跟design pattern里的class也很像，因为dp里面的class也可以hide,
plug...而且在讲述design
pattern的书中，大部分我们是靠着uml图来理解pattern的，根本不涉及内部具体实现。我想是不是应该这样理解：我们一般所指的
component是一个很单纯的概念，是一个完全的黑盒子；我们所指的class总是一个带有"body"的离不开具体实现的概念；而design
pattern的意义大概在二者之间，他教会你如何写出很component化的class，具有dp设计风格的class很适合作为
component，甚至可以说只要把实现"遮住"就是一个component了。只不过，毕竟dp是一个处于具体设计层面，而不是架构层面的思想，所以
dp还是要用"class"这个词，而没有直接提"component"。

重复一遍，class是底层设计中的概念，而component是高层设计中的概念。

rCOS是跟design pattern的思想有关联，但是我觉得也可以把rCOS理解为把pre/post condition, traces,
protocol, dynamic behavior analysis……等FM领域的东西跟design
pattern, component联系成一个整体的一个linking theory。这样我们就可以用形式化方法来研究高层架构问题了。

rCOS不谈connector。这是一个对component本质理解的问题，各家观点不同啊～"我们是否需要复杂的connector?"
这是个没有答案的问题。因为一般我们对connector的实现总是非常ad hoc的，而connector的语义很难跟component区分开来，所以这里是比较麻烦。

说到related works，类似的对component进行形式化的相关工作还不多。也就是说，rCOS就是最新技术～～

我对组件的assembly很感兴趣。世界上有无数的组件，怎么知道哪个是我想要的？给你一个组件，这个组件是不是我想要的组件？必需靠严格的精化证明
吗？看到片子后面似乎有这种感觉。其实，也可以考虑中间的容易一点的技术。刘老师说为此他才提出了"publication"的概念。还要再仔细研究publication是怎么回事，现在我只知道publication是contract的一部分。

因为这些component相关的概念是较高层设计中的概念，所以在informal的情形下，很容易变成一种泛泛而谈，让人难以捉摸的“方法学”；而当
我们把这些东西formalize之后，可以对组件列出他们的性质123，这样对他们的理解就深刻多了。所以说，formal
methods还是很有意义的。

什么是MOF(Meta Object Facility)

UML是用于表示模型的语言。UML Metamodel是表示UML的语言。那什么是表示UML Metamodel的语言？就是MOF了。

一个例子：XMI(XML Metadata Interchange) （天哪，这些缩写就够难理解了，没想到这些缩写的全称也还是让人无法理解……）

人们因为讨厌太多不同的语言细节，想统一的表达对模型的看法，所以使用UML作为交流、沟通的工具。于是产生了很多UML工具。于是，出现了一个新问题：
不同的UML工具保存的UML文件格式各不相同，比如Rose的格式跟Magic
Draw就不同。何不再"U"一下，把这些格式统一呢？所以就有了XMI这个统一的描述UML的XML规范。XMI is a way to save
UML models in XML, but more general than that. 反过来想一想，UML can be
regarded as an XML DTD to which UML models must conform。

model, meta-model, meta-meta model, meta-meta-meta model... 还好，通过xml schema，XML算是自定义的，这样就不会再出现下一层"meta"了！

XMI总结：XMI是一个基于MOF的语言。XMI shows how to save any MOF-based metamodel in XML.

---

以上有些是读来的观点，有些是个人的理解……不保证肯定正确...

发现一个有趣的事，我喜欢在blog上写些我不熟悉的东西；比如其实没学几天的B方法，还不太会用的pvs，刚刚接触不久的javascript，
emacs……其实，当我写下“什么是XXX”作为blog标题的时候，我其实是在说“我昨天还不懂XXX，今天看了几篇文章，懂了一点了”。

但是我真正熟稔于心的东西，像Model
checking，像好歹学过一个学期的Z，反而懒得写成blog了。。。因为很熟悉，反倒觉得写下来也只是重复，而起不到总结提高的效果。也因而失去了交流的机会……以后要稍微改变一下～

从一个小程序体会Javascript的强大表达能力

考虑写一个自动重复生成字符串的函数。如果输入"abcde", 5，就应该得到"abcdeabcdeabcdeabcdeabcde"。

最老土的写法是这个样子：function x(str,num){    var tmp = "";    for(var i=0;i
据说现在比较流行的写法是这样：
String.prototype.x = function(num){    for(var i=0,tmp="";ihttp://la.ma.la/blog/diary_200510060733.htm)





分类: 计算机技术
没有评论

“The Grand Challenge”

Grand Challenge是Tony Hoare和Jayadev Misra最近提出的一个口号。Hoare相信形式化方法进入应用的时代将要到来，为此我们要做哪些努力？文章作了一个50年的长期规划，但更多的是一种宣告：形式化方法离工业界已经不远了！

下载 :http://vstte.inf.ethz.ch/pdfs/vstte-hoare-misra.pdf

讨论Grand Challenge的wiki: http://vstte.inf.ethz.ch/wiki/。 这是个有趣的尝试。通过wiki，任何人都可以在第一时间领略到大牛们的思想观点甚至与之交流……大牛们可能没有时间写blog，wiki倒是一个不错的交流环境。

除了原文，这个关于Grand Chanllenge的FAQ: http://vstte.inf.ethz.ch/wiki/index.php/Verified_Software:_Frequently_Asked_Questions 也值得看看。摘录几则如下：

Q1. Why do you think that the time is ripe for a concerted effort of this nature?

A: The challenge of construction of a routinely usable Program
Verifier was first proposed in 1969 by Jim King in his Doctoral
Dissertation. Since that time, the power and capacity and sheer numbers
of installed computers have each increased more than a thousand-fold;
and a thousand-fold advance has been made in certain aspects of
mechanised theorem proving (e.g., SAT solving). There have been useful
conceptual advances in programming theory, and there is already useful
experience of construction of manual proofs for critical programs. The
cost of programming error to the economy of the world has similarly
escalated.

If all the advances in software and hardware technology can be
brought to bear in a coordinated project for the delivery of a program
verifier, the prospect of success is much greater than it ever has been
in the past. Even though the risks are still high, this is the kind of
challenge that must be attempted again; because the potential of reward
far outweighs the risk. Even in the event of failure, some beneficial
spin-off is likely; and another attempt will surely be made later.

Q2. It has been over 35 years since the publication of the
classic paper, An Axiomatic Basis of Computer Programming, by Tony
Hoare. Yet, very few schools teach formal methods in U.S.A. and most
practitioners avoid any formal work. What do you expect it will take to
effect a paradigm shift?

A: The existence (or even the near prospect) of an automatic
program verifier may well be the trigger for the necessary paradigm
shift. It may break the vicious circle of students who do not wish to
learn a technology that is not used in industry, and an industry that
is reluctant to apply a technology in which their recruits are not
trained.

The crucial motivation for education in the principles of
verification is that it is driven by scientific ideals, in that it
addresses the questions fundamental in all branches of engineering
science. For any product of engineering, the qualified engineer must be
able to answer questions on what it does and how it works. Scientists
should be able to answer deeper questions, explaining why it works, and
how we know that the answers to the previous questions are correct.
Even if the fundamental achievements of pure science seem remote from
practical application, good engineers and entrepreneurs eventually find
ways of exploiting established scientific theories and tools.

Q3. How will you educate managers, software designers and programmers for this paradigm shift?

A: There is good evidence that intellectually live programmers
can be educated in the principles and practice of specification and
verification. For example, the Department of Continuing Education at
Oxford runs a part-time Professional Development Masters Degree, which
attracts many students from the British software Industry. The United
Nations University in Macau has concentrated their research and
education on formal methods of software engineering. Their experience
is available to be exploited and generalised in the development of
tools and texts for general education.

Q4: How would you train verification engineers? Should they
have domain knowledge, say in banking or medical profession? What kind
of CS background should they have? How long should they be trained?

A: The patterns for professional education in other branches of
Engineering should be followed as closely as possible. A good general
engineering education is a mixture of mathematics, general science and
general engineering. It is illustrated by more detailed studies and
exercises in a particular domain of application. But good engineers
will always look forward to mastering or at least understanding many
other specialisations, as the need arises during their professional
career.

Q39: Is this challenge grand enough? Would it possibly suck
money away from other worthy projects where advances in basic sciences
can be made?

A: The initiation of a good scientific challenge should not be
dependent on any significant increase of funding. We could recommend
this project as just one of the more efficient ways of way of spending
whatever money is allocated for the advancement of Computer Science.
Because Science is cumulative, progress can be made, albeit more
slowly, even with the same absolute amounts of funding, provided the
funds are distributed wisely.

Because of the risks, we think it would be dangerous if this
project absorbed more than a few percent of the total world-wide
expenditure on research in Computer Science. Verification only solves
one of the problems of effective computer application, and continued
research support is essential in all the other areas relevant to the
delivery of dependable and useful software.

其实我想，如果大部分学校都采用Locig in Computer Science这样的好书作本科教材，那未来形式化方法的普及就比较有希望了....