The Semantics of Triveni: A process-Algebraic API for Threads + Events
Christopher Colby, Lalita Jategaonkar, Radha Jagadeesan, Konstantin Läufer, Carlos Puchol · Electronic Notes in Theoretical Computer Science · 1998
This paper describes compositional semantics (operational, denotational and logical) for a process algebra enhanced with input/output actions and preemption combinators, in the presence of fairness. The context of this paper is Triveni, a process-algebra-based design methodology that combines threads and events in the context of object-oriented programming. Triveni has been realized as an Application Programmer Interface in the Java programming language. The semantics described in this paper forms the theoretical basis of the Triveni programming language and environment. (i) The operational model described in this paper is the precise formalization of the implementation. (ii) The denotational semantics serves as the basis for a non-definability result. This result justifies the introduction of certain powerful preemption combinators as primitives in Triveni. (iii) The logical semantics forms the basis of our specification-based testing environment realized in the implementation.