```
@Documented
@Retention(RUNTIME)
@Target({METHOD,CONSTRUCTOR})
public @interface TerminatesExecution
```
TerminatesExecution is a method annotation that indicates that a method terminates the execution of the program. This can be used to annotate methods such as System.exit(), or methods that unconditionally throw an exception.
The annotation enables flow-sensitive type refinement to be more precise. For example, after
```
 if (x == null) {
   System.err.println("Bad value supplied");
   System.exit(1);
 }
 
```
the Nullness Checker can determine that x is non-null.
The annotation is a trusted annotation, meaning that it is not checked whether the annotated method really does terminate the program.
This annotation is inherited by subtypes, just as if it were meta-annotated with @InheritedAnnotation.
The Checker Framework recognizes this annotation, but the Java compiler javac does not. After calling a method annotated with TerminatesExecution, to prevent a javac diagnostic, you generally need to insert a throw statement (which you know will never execute):
```
 ...
 myTerminatingMethod();
 throw new Error("unreachable");
 
```
See the Checker Framework Manual:
Automatic type refinement (flow-sensitive type qualifier inference)

Annotation Type TerminatesExecution