“宏观经济学发生了一个与电影十分类似的转向：即令人目眩神迷的特技越来越多，可是情节简单化的情况也越来越普遍。人们其实盼望出现这样一种宏观经济学，其情节（而不是特技）将给人类状况带来更多的启示。” （见 武夷山老师博文 《主流之外的经济学家Axel Leijonhufvud》）

     在某种意义上，形式化方法就是特技。 形式化方法是需要的，就如同维C，但是不能当饭吃。更多时，形式化方法起着锦上添花之用。反之，过犹不及。看过一些论文，明明是很简单的内容，应用了形式化方法，一是概念满天飞，二是定理证明应接不暇。引用我喜欢的一本书《虚拟机的设计与实现 C/C++》

   "While I was a graduate student, I learned a dirty little secret about how to get research published. If a professor makes a discovery that can be explained in simple terms, he will go to great lengths and use any number of obfuscation techniques to make the discovery look more complicated than it really is. This is more of a sociological phenomenon than anything else. The train of thought behind this is that if an idea is simple, then it must not be very revolutionary or clever. People who referee journal submissions are more likely to be impressed by an explanation that wraps around itself into a vast Gordian knot.

This may work for professors who want tenure, but it sure doesn't work for software engineers. In his Turing Award lecture, "On Building Systems that will Fail," one of the conclusions Fernando Corbató makes is that sticking to a simple design is necessary for avoiding project failure. You should listen to this man. Corbató is a voice of experience and one of the founding fathers of modern system design. He led the project to build MULTICS back in the 1960s."

   

     过于崇尚形式化的学者多是数学出身，几乎没有编过程序，不知道程序员需要什么？而是一味将数学理论套用于 计算 理论中，也不管是不是适用？一个UML，国内外多少人加形式语义灌水？

   学院派：研究在于新，研究一些与众不同的新玩艺，至于有没有用，天知道！关键是在理论层面能够自圆其说。

   工程派：开发项目并不追求新奇算法、理论等，但要实用，满足工程指标。

怎么办？A Delicate Balance！How to trade off? This is a question?

   

 

 

Abstract
   Temporal logic is obtained by adding temporal connectives to
a logic language. Explicit references to time are hidden inside
the temporal connectives. Dierent variants of temporal logic
use dierent sets of such connectives. In this chapter, we survey
the fundamental varieties of temporal logic and describe their
applications in information systems.
  Several features of temporal logic make it especially attractive as
a query and integrity constraint language for temporal databases.
First, because the references to time are hidden, queries and integrity
constraints are formulated in an abstract, representationindependent
way. Second, temporal logic is amenable to ecient
implementation. Temporal logic queries can be translated to an
algebraic language. Temporal logic constraints can be eciently
enforced using auxiliary stored information. More general languages,
with explicit references to time, do not share these properties.
  Recent research has proposed various implementation techniques
to make temporal logic practically useful in database applications.
Also, the relationships between dierent varieties of temporal
logic and between temporal logic and other temporal languages
have been claried. We report on these developments and
outline some of the remaining open research problems.

    Temporal Logic in Information Systems.pdf