Information Technology Reference
In-Depth Information
The pattern description provide information that can be very useful in veri-
fying that an actual design or implementation actually is in accordance with the
intent of the pattern.
Implementation: A Singleton is usually implemented as a class with a protected
constructor as the only constructor. This should prevent external use of new to
generate more instances. The instance of the Singleton is created first time the
Instance() method is called. This call looks up the private instance attribute to
see if it exists, and if it is not an instance is created, assigned and returned to
the caller. For future calls the instance is returned.
Functional Verification Conditions: The Singleton pattern is a creational pat-
tern, where there as such is not much to verify. There is an invariant stating
that the instance reference is valid and that it is not changed unless it is null by
the Instance operation. The pre-condition for the Instance operation is trivially
true and the post-condition states that the result of the operations is a copy of
the reference to this instance.
Behavioural Verification Conditions: There is one specified behaviour
main == s.Instance !( y == s.instance )
main
When applying a singleton pattern with class s , we do not have to take any
special precautions, the assert is trivially true .Atanypoint,wecan assume
that there is at most one instance of the class and that this instance remains the
same, i.e. it is not overwritten. Thus combining the functional and behavioural
condition, we can prove that an application satisfies the property that
( s.Instance ? y : Singleton
P ( y ))
(( s.Instance ? y : Singleton
Q ( y ))
is equivalent with
( s.Instance ? y : Singleton
( P ( y ))
Q ( y ))
Thus, we can eliminate or introduce (using CSP laws) multiple calls of Instance .
The idea of exploiting a design using design patterns to extract verification
lemmas is in Example 1 made less abstract as the use of a Singleton patterns is
embedded in a design.
Example 1. On a modern ship the rudder can be manipulated and monitored
from various stations on the ship. Here it is relevant to consider the rudder
controller as a Singleton. In this example the rudder can be manipulated from
the ship bridge and from the machine room.
In Figure 3 the UML diagram illustrates a design where the classes Bridge
and Machine both have a RudderSingleton object. Although UML allows
specification of the arity between objects by annotating the edges between them,
in Figure 3 by 1's at the RudderSingleton class, this only states that one Bridge
 
Search WWH ::




Custom Search