Formal Semantics of Orc Based on TLA(

Concurrency is ubiquitous today. Orc provides four powerful combinators (parallel combinator, sequential combinator, pruning combinator and otherwise combinator), used to structured concurrent programming in a simple and hierarchical manner. In order to extend concurrent mechanism in our abstract sequential programming language, called Apla, we have already done some research about Orc. The paper takes a step towards this goal by presenting formal semantics of Orc based on TLA\(^+\) language. Compared with other semantics of Orc, our major concern is Orc expression’s next-state relation/action, which is ideal for expressing behavior of a sequence of states. And liveness properties of Orc expression are also elaborated by using TLA\(^+\) weak fairness. After analysis and comparison, our proposal could be simpler to illustrate specification of Orc program via the well known dining philosophers problem.