mjc

org.multijava.mjc
Class CVariableState

java.lang.Object
  extended byorg.multijava.mjc.CVariableState
All Implemented Interfaces:
Cloneable

public class CVariableState
extends Object
implements Cloneable

The class stores information about the definitely assigned state of a variable or field. See JLS2, chapter 16.

Version:
$Revision: 1.16 $
Author:
Curtis Clifton

Field Summary
private  boolean isDefinitelyAssigned
          Indicates that the variable represented by this definitely has been initialized.
private  boolean maybeAssigned
          Indicates that the variable represented by this may have been initialized.
private  VariableDescriptor variableDesc
          A descriptor for the field or variable (i.e., slot) tracked by this state.
 
Constructor Summary
CVariableState()
          Create a variable state corresponding to a newly allocated variable.
 
Method Summary
 Object clone()
           
 CVariableState duplicate()
          Returns a duplicate of this.
 boolean equals(Object other)
           
 int hashCode()
           
 String ident()
          Returns the (unqualified) identifier of the slot tracked by this.
 void initialize()
          Mutates the state of this to indicate that the corresponding variable has been initialized in the local control flow.
 boolean isDefinitelyAssigned()
          Returns true if the variable represented by this is definitely initialized (i.e., is definitely assigned according to JLS2, 16).
 boolean isDefinitelyUnassigned()
          Returns true if the variable represented by this is definitely not initialized (i.e., is definitely unassigned according to JLS2, 16).
 boolean isFinal()
          Returns true if the slot tracked by this is declared final.
 CVariableState mergeWith(CVariableState other)
          Mutates the state of this to indicate the result of merging with the given variable state.
 void setDescriptor(VariableDescriptor varDesc)
          Sets the descriptor of the slot whose state is tracked by this.
 String toString()
           
 void tryFinallyMergeWith(CVariableState tryVariableState)
          Sets the definite assignment state of this using the special merge logic appropriate for combining the definite assignment information from a finally block (as represented by this) with the definite assignment information from a try-block.
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

maybeAssigned

private boolean maybeAssigned
Indicates that the variable represented by this may have been initialized.


isDefinitelyAssigned

private boolean isDefinitelyAssigned
Indicates that the variable represented by this definitely has been initialized.


variableDesc

private VariableDescriptor variableDesc
A descriptor for the field or variable (i.e., slot) tracked by this state. Descriptor is only initialized if the slot may be initialized.

Constructor Detail

CVariableState

public CVariableState()
Create a variable state corresponding to a newly allocated variable.

Method Detail

clone

public Object clone()
Overrides:
clone in class Object

toString

public String toString()
Overrides:
toString in class Object

duplicate

public CVariableState duplicate()
Returns a duplicate of this. Utility method allows clients to avoid typecast when cloning this.


 ensures \fresh(\result) && \result.equals(this);
 


isDefinitelyAssigned

public boolean isDefinitelyAssigned()
Returns true if the variable represented by this is definitely initialized (i.e., is definitely assigned according to JLS2, 16).


isDefinitelyUnassigned

public boolean isDefinitelyUnassigned()
Returns true if the variable represented by this is definitely not initialized (i.e., is definitely unassigned according to JLS2, 16).


initialize

public void initialize()
Mutates the state of this to indicate that the corresponding variable has been initialized in the local control flow.


mergeWith

public CVariableState mergeWith(CVariableState other)
Mutates the state of this to indicate the result of merging with the given variable state.

 {|
   requires other == null;
   modifiable objectState;
   ensures (* result is equivalent to the case where other != null &&
              other.isDefinitelyUnassigned() *);
   ensures \result == this;
 |}
 also
 {|
   requires other != null;
   modifiable objectState;
   ensures (* mergeWith is symmetric *);
 
   ensures \old(this.isDefinitelyAssigned()) &&
 		other.isDefinitelyAssigned()
   		==> \result.isDefinitelyAssigned();
 
   ensures \old(this.isDefinitelyAssigned()) &&
 		!other.isDefinitelyAssigned()
   	 	==> !\result.isDefinitelyUnassigned() &&
 				!\result.isDefinitelyAssigned();
 
   ensures \old(this.isDefinitelyUnassigned()) &&
 		other.isDefinitelyUnassigned()
 			==> \result.isDefinitelyUnassigned();
 
   ensures \old(!this.isDefinitelyAssigned() &&
 			!this.isDefinitelyUnassigned()) &&
 		!other.isDefinitelyAssigned()
   	 	==> !\result.isDefinitelyUnassigned() &&
 				!\result.isDefinitelyAssigned();
   ensures \result == this;
 |}
 


tryFinallyMergeWith

public void tryFinallyMergeWith(CVariableState tryVariableState)
Sets the definite assignment state of this using the special merge logic appropriate for combining the definite assignment information from a finally block (as represented by this) with the definite assignment information from a try-block.

Parameters:
tryVariableState - definite assignment state from a try block

equals

public boolean equals(Object other)
Overrides:
equals in class Object

hashCode

public int hashCode()
Overrides:
hashCode in class Object

setDescriptor

public void setDescriptor(VariableDescriptor varDesc)
Sets the descriptor of the slot whose state is tracked by this.


isFinal

public boolean isFinal()
Returns true if the slot tracked by this is declared final. Result is only valid if maybeAssigned.


ident

public String ident()
Returns the (unqualified) identifier of the slot tracked by this. Result is only valid if maybeAssigned.


mjc

mjc is Copyright (C) 2000-2004 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. mjc is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.