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 and the output channels for