Advertisement
Published in:
2009 | OriginalPaper | Chapter
Object-Oriented Programs
Published in: Verification of Sequential and Concurrent Programs
Publisher: Springer London
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
In This Chapter we study the verification of object-oriented programs. We focus on the following main characteristics of objects:
objects possess (and
encapsulate
) their own local variables,
objects interact via
method
calls,
objects can be dynamically
created
.
In contrast to the formal parameters of procedures and the local variables of block statements which only exist
temporarily
, the local variables of an object exist
permanently
. To emphasize the difference between these temporary variables and the local variables of an object, the latter are called
instance
variables. The local state of an object is a mapping that assigns values to its instance variables. Each object represents its local state by a
pointer
to it.
Encapsulation means
that the instance variables of an object cannot be directly accessed by other objects; they can be accessed only via method calls of the object.