Handbook of Truly Concurrent Process Algebra

Chapter 35: Verification of idioms

Abstract

This chapter introduces the verification of Idioms based on truly concurrent process algebra.

Keywords

Idioms; Verification; Process Algebra

Idioms are the lowest-level patterns that are programming language-specific and implement some specific concrete problems.

There are numerous language-specific idioms, in this chapter, we only verify two idioms called the Singleton pattern and the Counted Pointer pattern.

35.1 Verification of the Singleton pattern

The Singleton pattern ensures that there is only one instance in runtime for an object. In the Singleton pattern, there is only one module: The Singleton. The Singleton interacts with the outside through the input channels $I_i$ and the output channels $O_i$ for