Inferring object invariant method and system
First Claim
1. A computer implemented method for determining invariants within an object oriented program, comprising:
- at least partially running a local analysis of the program wherein the local analysis notes at least one local value of at least one object field at at least one program point;
at least partially running a global analysis of the program, wherein an object is either mutable or valid;
wherein the global analysis stores at least one value which the object field has held when the object is valid; and
combining the local analysis and the global analysis to infer at least one invariant for at least one object, wherein the combining comprises the local analysis reaching a program point wherein the object transitions from mutable to valid, the local value of the at least one object field being given to the global analysis, this value within the global analysis comprising the global analysis information about the object.
2 Assignments
0 Petitions
Accused Products
Abstract
A local analysis analyzes the values of objects paying attention to program flow and a global analysis analyses the object independent of the flow. The local and global analysis interact to infer the invariants of objects used within a computer program. The local analysis is given the known invariants of an object by the global analysis when the object transitions from a valid to a mutable state. It then keeps track of all of the values of objects encountered until the object transitions from mutable to a valid state, when the information known to the local analysis is passed to the global analysis, which may use the new object values to add to the current list of invariants for the given object.
33 Citations
20 Claims
-
1. A computer implemented method for determining invariants within an object oriented program, comprising:
-
at least partially running a local analysis of the program wherein the local analysis notes at least one local value of at least one object field at at least one program point;
at least partially running a global analysis of the program, wherein an object is either mutable or valid;
wherein the global analysis stores at least one value which the object field has held when the object is valid; and
combining the local analysis and the global analysis to infer at least one invariant for at least one object, wherein the combining comprises the local analysis reaching a program point wherein the object transitions from mutable to valid, the local value of the at least one object field being given to the global analysis, this value within the global analysis comprising the global analysis information about the object. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9)
-
-
10. At least one computer-readable medium having stored thereon a representation of invariant states of a sequential computer program, the invariant state representation comprising:
-
a representation of a flow-sensitive value state wherein the representation comprises a representation of the values of at least one object encountered between two program points; and
a representation of a flow-insensitive value state wherein the representation comprises a representation of substantially all of the values for substantially all of the objects encountered up to a given program point;
wherein the flow-sensitive analysis state and the flow-insensitive analysis state exchange information at least one exchange program point. - View Dependent Claims (11, 12, 13)
-
-
14. A computer system for inferring invariant states of objects, the computer system comprising
a compiler operable for generating the invariant states from a source code representation of the computer program, wherein the source code representation comprises one or more objects, each object comprising one or more fields with values; -
a flow sensitive analysis module for generating at least a partial flow sensitive invariant storage which stores essentially all possible values of at least some object fields between two program points;
a flow insensitive analysis module for generating at least a partial flow insensitive invariant storage which stores essentially all possible values that at least some object fields have held from a first program point to an intermediate program point;
a mutable location module for during the generation locating a location wherein for an object O the object O is moving from a valid to a mutable state; and
a flow insensitive instantiation module which instantiates the partial flow insensitive analysis invariant state for object O within the at least partial flow sensitive analysis invariant state. - View Dependent Claims (15, 16, 17, 18, 19, 20)
-
Specification