You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: reference/external-refinements.md
+22-15Lines changed: 22 additions & 15 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -1,35 +1,42 @@
1
1
---
2
2
title: External Refinements
3
3
parent: Reference
4
-
nav_order: 5
4
+
nav_order: 4
5
5
---
6
6
7
7
# External Refinements
8
8
9
-
External refinements let you attach a LiquidJava model to an existing class that you do not own.
9
+
External refinements let us add refinements to an existing class that we cannot modify.
10
10
11
-
Use `@ExternalRefinementsFor` to describe the behavior of a library type in a separate interface. This lets you keep using the original library API in ordinary Java code while LiquidJava checks the extra specification in the background.
11
+
For this, we use the `@ExternalRefinementsFor`annotation to specify the qualified name of the class we want to refine in a separate interface. This lets us refine external classes from the Java standard library, third-party dependencies, or shared APIs without modifying their source code.
This pattern is useful when you want to verify protocols for standard-library classes, third-party dependencies, or shared APIs without modifying their source code.
37
+
```java
38
+
Socket socket =newSocket();
39
+
socket.connect(newInetSocketAddress("example.com", 80)); // type error!
40
+
socket.close();
41
+
```
34
42
35
-
The [Examples]({{ '/examples/' | relative_url }}) page links to runnable repositories that include this style of modeling.
Some protocols need more than a small set of named states. LiquidJava supports ghost variables for tracking extra state. They can be used in refinements and state refinements to express richer invariants about the object. Similarly to the states, these are functions that take the object being refined as a parameter.
10
+
11
+
Ghosts are declared with the `@Ghost` annotation, and they can be updated with `@StateRefinement` annotations on methods.
In the "constructor" method, the ghost variable `size` is initialized to 0. An equality in a method postcondition is how ghost variables are updated. However, here it is not necessary, since when no postcondition is declared, it is initialized to its default value, similarly to how Java initializes fields to their default values when no explicit initializer is provided (`int --> 0`, `boolean --> false`, etc.).
42
+
43
+
In the `push` method, we specify no precondition, since we can always push an element to the stack, but we specify a postcondition that increments the `size` by one. In this case, we tell the typechecker that the new value of `size` after calling `push` is equal to the old value of `size` plus one. This is possible using the `old` function, which takes an object instance and returns its value before the method call.
44
+
45
+
In the `pop` method, we specify a precondition that the `size` must be greater than zero, since we cannot pop from an empty stack. We also specify a postcondition that decrements the `size` by one, similarly to the `push` method.
46
+
47
+
In the `peek` method, we specify the same precondition, since we also cannot peek from an empty stack, but we don't specify a postcondition since peeking does not change the size of the stack.
@Refinement("0 <= _ && _ <= 100") // y must be between 0 and 100
21
-
int y;
21
+
int y=50;
22
22
23
23
@Refinement("z % 2 == 0 ? z >= 0 : z < 0") // z must be positive if even, negative if odd
24
-
int z;
24
+
int z=4;
25
25
26
26
@Refinement("_ >= 0") // the return value must be non-negative
27
27
intabsDiv(inta, @Refinement("b != 0") intb) { // b must be non-zero
@@ -33,7 +33,7 @@ public class RefinementExamples {
33
33
34
34
## Predicate Syntax
35
35
36
-
The predicates allowed inside a refinement belong to quantifier-free linear integer arithmetic. In practice, this means you can write boolean expressions over integer values using comparisons, logical connectives, arithmetic operators, and conditional expressions. You can also call ghost variables and aliases from refinements, which we cover in later sections.
36
+
The predicates allowed inside a refinement belong to quantifier-free linear integer arithmetic. In practice, this means you can write boolean expressions over integer values using comparisons, logical connectives, arithmetic operators, and conditional expressions. You can also call ghosts and aliases from refinements, which we cover in later sections.
Copy file name to clipboardExpand all lines: reference/state-refinements.md
+61-22Lines changed: 61 additions & 22 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -8,45 +8,84 @@ nav_order: 3
8
8
9
9
Beyond basic refinements, LiquidJava supports object state modeling through typestates. This lets you describe when a method can or cannot be called based on the state of the object.
10
10
11
-
## Example
11
+
The possible states of a class are declared with `@StateSet`, and the state transitions are described with `@StateRefinement(from = "...", to = "...")`:
12
+
-`from` describes the **precondition** - the object state in which the method can be invoked
13
+
-`to` describes the **postcondition** - the state the object will have after the method is called
12
14
13
15
```java
14
-
importliquidjava.specification.StateRefinement;
15
-
importliquidjava.specification.StateSet;
16
+
importliquidjava.specification.*;
16
17
17
18
@StateSet({"open", "closed"})
18
-
publicclassMyFile {
19
-
@StateRefinement(to="open(this)")
20
-
publicMyFile() {}
19
+
publicclassFile {
20
+
@StateRefinement(to="open()")
21
+
publicFile() {}
21
22
22
-
@StateRefinement(from="open(this)", msg="file must be open to read")
23
+
@StateRefinement(from="open()")
23
24
publicvoidread() {}
24
25
25
-
@StateRefinement(from="open(this)", to="closed(this)", msg="file must be open to close")
26
+
@StateRefinement(from="open()", to="closed()")
26
27
publicvoidclose() {}
27
28
}
29
+
```
28
30
29
-
MyFile f =newMyFile();
31
+
```java
32
+
File f =newFile();
30
33
f.read();
31
34
f.close();
32
-
f.read(); // type error: file must be open to read
35
+
f.read(); // type error!
36
+
```
37
+
38
+
If a class follows an implicit protocol that can be described by a DFA, the protocol can be encoded in LiquidJava so that methods are enforced to be called in the correct order.
39
+
40
+
## Syntax
41
+
42
+
Note that states are functions. These take a single parameter, which is the object being refined. Since we are describing the state of the current object, we use `this` as the parameter, which is being used implicitly in the example above. Actually, all of these are equivalent: `open()`, `this.open()`, and `open(this)`.
43
+
44
+
## State Initialization
45
+
46
+
Constructors can only declare a `to` transition, since they are responsible for establishing the initial state of the object.
47
+
48
+
```java
49
+
importliquidjava.specification.*;
50
+
51
+
@StateSet({"new", "ready"})
52
+
publicclassBuffer {
53
+
@StateRefinement(to="ready()")
54
+
publicBuffer() {}
55
+
}
33
56
```
34
57
35
-
This encodes a simple protocol:
58
+
If no `to` transition is written, LiquidJava defaults the constructor to the first state listed in the corresponding `@StateSet`.
36
59
37
-
- construction produces an open file
38
-
-`read` requires the file to be open
39
-
-`close` requires the file to be open and transitions it to closed
60
+
Constructors must always be present for typestate checking to work correctly, because they are the point where the initial state values are assigned. Otherwise, the initial values are not set and the verifier won't be able to track the state of the object across method calls, which can lead to unexpected type errors.
40
61
41
-
An illegal call sequence, such as reading after closing, becomes a verification error. As with refinements, you can provide custom error messages to make violations easier to diagnose.
62
+
When refining interfaces, there is no real constructor, but LiquidJava still needs an initialization point. In those cases, if the type is named `Interface`, it must declare a method with the signature `public void Interface()` so the initial values are set correctly. This method plays the role of a constructor for the typestate system.
42
63
43
-
## Why This Matters
44
64
45
-
Typestates are especially helpful for:
65
+
## Multiple StateSets
66
+
67
+
Classes can declare more than one `@StateSet` annotation. This is useful when the object has independent, orthogonal dimensions of state.
Each state set is exclusive: at any moment, the object can only be in one state from that specific set. In the example above, the object cannot be both `open` and `closed`, and it cannot be both `clean` and `dirty`.
51
90
52
-
Continue with [Ghost Variables]({{ '/reference/ghost-variables/' | relative_url }}) and [External Refinements]({{ '/reference/external-refinements/' | relative_url }}) for protocols that need richer tracking.
91
+
When a transition affects multiple orthogonal states, the states must be combined with `&&` in the `from` and `to` annotations. In the example above, the `use` method transitions from `open && clean` to `open && dirty`, and the `close` method transitions from `open && clean` to `closed && clean`.
0 commit comments