Unifying Theories of Programming - 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers
Unifying Theories of Programming - 5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers
复制标题
统一编程理论 - 第五届国际研讨会，UTP 2014，新加坡，2014 年 5 月 13 日，修订后的精选论文
DOI：
10.1007/978-3-319-14806-9_1
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Canham S
中科院分区：
文献类型：
--
作者：
Canham S
我们探索不同的方法，将外部选择建模为具有离散时间的 UTP 语义中的反应过程。外部选择的标准定义不能简单地在定时语义中重用，因为它可能引入非前缀封闭的行为和立即发生的紧急事件。我们首先检查 CSP 不同语义中的不稳定状态和紧急事件。我们提出了一种简单的定时反应式 UTP 语言的语义，并描述了添加外部选择的困难。我们定义了两个新的流程操作符：严格选择（从不参与紧急事件）和惰性选择（可以延迟紧急事件）。我们简要讨论了语言模型的两个潜在修改；懒惰语义，其中终止不是不稳定的，以及可以观察到不稳定状态的语义。最后，我们对严格选择进行更详细的处理，将其表示为反应式设计并陈述其代数定律。
We explore different approaches to modelling external choice as a reactive process in a UTP semantics with discrete time. The standard definition of external choice cannot be simply reused in a timed semantics, since it can introduces behaviours which are not prefix-closed and urgent events which occur instantly. We first examine unstable states and urgent events in different semantics for CSP. We present the semantics for a simple timed reactive UTP language and describe the difficulties of adding external choice. We define two new process operators;strict choice, which never engages in urgent events andlazy choice, which can delay urgent events. We briefly discuss two potential modifications to the language model; alazy semantics, in which termination is not unstable, and a semantics in which unstable states can be observed. Finally, we give a more detailed treatment to strict choice, expressing it as a reactive design and stating its algebraic laws.