1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
<!DOCTYPE html>
<html>
<head>
<title>Checker Framework quick start guide</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
</head>
<body>
<h1>Checker Framework quick start guide</h1>
<p>
This document gives some important information for getting started with
pluggable type-checking. More resources are given at the end.
</p>
<p>
A pluggable type-checker, or “checker” for short, prevents certain run-time errors. For example, it can prove that your code never suffers a
NullPointerException. Choose which checker you want to run from the <a href="https://checkerframework.org/manual/#introduction">list
of checkers</a>.
</p>
<p>
To <a href="https://checkerframework.org/manual/#installation">install the Checker Framework</a>, download and unzip
the Checker Framework distribution:
<a href="checker-framework-2.1.7.zip"><!-- checker-framework-zip-version -->checker-framework-2.1.7.zip<!-- /checker-framework-zip-version --></a>.<br/>
Or, the
<a href="http://eisop.uwaterloo.ca/live/">Checker Framework Live Demo</a>
webpage lets you try the Checker Framework without installing it.
</p>
<p>
To <a href="https://checkerframework.org/manual/#running">run a checker</a>, supply the <code>-processor</code> command-line argument:
</p>
<pre>
$CHECKERFRAMEWORK/bin/checker/javac -processor nullness MyFile1.java MyFile2.java
</pre>
<p>
You write annotations in your code. Then, the checker
<a href="https://checkerframework.org/manual/#checker-guarantees">verifies
two facts:</a> (1) the annotations you wrote are correct (they are consistent with your source code), and (2) your program will not suffer certain exceptions or errors at run time.
</p>
<p>
Java has two types of annotations: type annotations and declaration annotations.
</p>
<ul>
<li>
A type annotation, also known as a type qualifier, creates a new type. The
qualified type represents a different set of values. For example, the
ordinary Java type <code>String</code> includes <code>"hello"</code>,
<code>""</code>, <code>null</code>, and other values. The
<code>@NonNull String</code> type includes <code>"hello"</code> and
<code>""</code>, but does not include <code>null</code>.
<br/>
You write a type annotation right before a use of a type (on the same
line), <a href="https://checkerframework.org/manual/#writing-annotations">as in</a>:
<pre>
@NonNull String s;
List<@Positive Integer> l;
class Folder<F extends @Existing File> { ... }
</pre>
</li>
<li>
A declaration annotation gives information about a method or a variable (as
opposed to information about the method's return type or the variable's
type).
<br/>
Write a declaration annotation on a different line than the declaration it
annotates. For example, to indicate that a method has no side effects:
<pre>
@SideEffectFree
public String toString() { ... }
</pre>
</li>
</ul>
<p>
For the most part, you only need to write annotations on method signatures and fields.
Most annotations within method bodies are <a href="https://checkerframework.org/manual/#type-refinement">inferred for you automatically</a>.
Furthermore, each checker applies certain defaults to further reduce your
annotation burden; for example, using the
<a href="https://checkerframework.org/manual/#nullness-checker">Nullness
Checker</a>, you do not need to write <code>@NonNull</code>, only
<code>@Nullable</code> which appears less often.
See the manual for more
<a href="https://checkerframework.org/manual/#tips-about-writing-annotations">tips
about writing annotations</a>.
</p>
<p>
To learn more, you can read:
</p>
<ul>
<li><a href="https://checkerframework.org/tutorial/">Checker Framework tutorial</a>
</li>
<li><a href="https://github.com/glts/safer-spring-petclinic/wiki">Nullness Checker tutorial</a> (external site, setup information is out of date)</li>
<li><a href="https://checkerframework.org/manual/#faq">Checker Framework frequently asked questions (FAQs)</a>
</li>
<li><a href="https://checkerframework.org/manual/">Checker Framework manual</a>
</li>
</ul>
</body>
</html>
|
