Hypothetical class for reading and writing files:

class File {
  public static final UNINITIALIZED=0;
  public static final OPEN=1;
  public static final CLOSED=2;
 
  int state = UNINITIALIZED
 
  [typestate: UNINITIALIZED -> OPEN]
  public void open(name : String) { ... }
 
  [typestate: OPEN]
  public String readLine() { ... }
 
  [typestate: OPEN]
  public void writeLine(String line) { ... }
 
  [typestate: OPEN -> CLOSED]
  void close() { ... }
}

Client code using File class:

   File f = new File();
   f.open("myfile.txt");     // ok
   ...
   f.write("someContent");   // ok
   ...
   f.close();                // ok
   ...
   f.write("moreContent");   // ERROR: file is closed

How can a compiler ensure absence of such errors?

For local variables: use initialization or liveness analysis

How to analyze this precisely?

• seen simple typestate analysis in Initialization Analysis

The Fugue protocol checker

• shows uses of typestate for properties beyond initialization: usage of library protocols

Extending Typestate Checking Using Conditional Liveness Analysis

• lattice contains for each variable its conditional liveness
• conditional liveness says that variable is live if certain integer variables belong to certain ranges
• in this paper, range is a union of disjoint intervals
• the meaning of element is that variable is not live unless the condition holds
• here and in general, do not get confused if the authors decide to swap the meaning of and , and , and . This is only a matter of notation.
• the paper does not address aliasing

Example:

f1 = new File()
f3 = new File();
f2 = f1;
f1.open("myfile.txt");
f3.open("anotherFile.txt");
f2.write("some content"); // ok
f1.close();
f3.write("different content");
f2.write("more content"); // ERROR

Need to know whether can hold or not

• when we store File-s into data structures, we must use alias analysis

Formally, references are functions from objects to objects

To know if one change affects the other, must know if function arguments are the same

• alias analysis approximately answers this question

p1 and p2 may alias: means 'true', we do not know anything

p1 and p2 may not alias: means that they are always different

p1 and m2 must alias: means that they are always the same

The terminology of may and must is used similarly

• “may” means that we don't know anything

Analogous situation with global arrays:

a[i] = 42;   // a[i] in [42,42]
a[k] = 7;   //  a[k] in [7,7], a[i] in ???

i=k?