Temporal logic provided an appealing approach to specifying properties of operating systems and other "reactive" software by allowing propositions to be qualified by "when" they must be true. This paper shows how to get the same effect, with a finer control over specification and a compositional notion of state, using ordinary working mathematics, without the weight of formal logic, by using sequential functions which are an alternate representation of Moore type state machines.
翻译:时序逻辑通过允许命题被限定为必须在"何时"为真,为操作系统及其他"反应式"软件的性质规约提供了一种引人注目的方法。本文展示了如何通过使用顺序函数(即Moore型状态机的替代表示),在避免形式逻辑繁复负担的前提下,利用常规工作数学实现同等效果,同时获得更精细的规约控制与组合化的状态概念。