How to annotate your code:

(with the Typestate automaton)

@TypestateChecked
class MyFile {
 
    @SetState( to="Init" )
    MyFile(boolean ch) { ... }
 
    @RequireState( isIn="Open" )
    int read() { ... }
 
    @SetState( to="Open" )
    void open() { ... }
 
    @ChangeState( from="Open", to="Closed")
    void close() { ... }
 
    @TS({
      @ChangeState( from="Closed", to="Closed" ),
      @ChangeState( from="Open", to="Closed" )
    })
    void secureClose() { ... }
 
    @NoStateChanges
    String name() { ... }
}
 

Type-state model annotations:

• @SetState: Set the type state to a specified state no matter which state the object is in (overwrites
  even the hidden error state)
• @ChangeState: Changes the type state from one specified state to a list of states. If this
  method is invoked the analysis verifies that the object is in the from state and then sets the new
  type state.
• @RequireState: Require one specific or one out of several specified states. This annotation is
  equivalent to a @ChangeState annotation form and to the same state.
• @TS : This is a wrapper for several @ChangeState annotations, because Java does not allow several annotation of the same annotation type. Naturally only one of the @ChangeState’s “from” states has to be fulfilled by the receiver. It is also possible to have the same “from” state
  several times if needed.
• @TypestateChecked: This annotation tells the type-state verifying algorithm that all methods of
  this class or interface have to be annotated. If this is not specified methods without annotation
  are assumed to have no effect on the type state.
• @NoStateChange: The Checker can be put in a mode that enforce annotations. In this mode
  every method has to be annotated. Methods that do not change the type state will have to be
  annotated with this annotation.
• @ScopeEndStates: If a usage protocol requires the object to be in one or several specified states
  at the moment at which no reference is left which points to it, use this annotation.
•  @ReturnValue: Verify that the return value of the method that is always in one of the states
  that are specified.                   

Typestate requirements on method parameters

The @RequireState, @SetState and the @ChangeState are not only used to annotate the type-state
automaton but are also used to annotate method parameters. The algorithm then also enforces
that all arguments passed as method parameters that are annotated with the @RequireState and
@ChangeState passed to the method are in the required type state and in the case of the @Change-
State and @SetState annotation updates the type state of the passed argument. Furthermore
parameters with the @SetState annotation are initialized to an undefined type state, meaning
the first method that changes the type state for those parameters has to be a method that is
setting the type state and not changing it.