莱斯利·兰波特的作品

2020-05-29 08:40:59

实时非常简单Microsoft Research TechnicalReport MSR-TR-2005-30(2005年3月4日)。在系统设计中被FormalMethods拒绝。可用性在线应该很明显,不需要特殊的逻辑或语言来编写实时规范或对其进行推理。有一种简单的方法可以做到这一点:只需使用变量来表示时间。马丁·阿巴迪和我在[106]一书中表明,在TLA中可以非常优雅地做到这一点。一种更简单、更直接的方法适用于任何明智的正式方法,但它过于简单和明显的浮夸。因此,我们可以使用更简单、更直接的方法来编写或推理实时规范。但有一种简单的方法太简单,也太明显的浮夸。因此,我在[106]一书中展示了这一点。更简单、更直截了当的方法适用于任何明智的正式方法,但它过于简单和明显的浮夸。等等。没有理由用它们来代替简单、明显的方法。而且,由于没有人写关于处理实时的简单方法的论文,人们似乎认为他们需要使用实时逻辑。很自然,我觉得这相当烦人。所以当我听说一位计算机科学家正计划写一本关于这些实时逻辑之一的书时,我决定是时候再写一篇论文来解释这种简单的方法了。(所以当我听说一位计算机科学家正计划写一本关于其中一种实时逻辑的书时,我决定是时候再写一篇论文来解释这种简单的方法了。)