Skip to content

Commit 1efe64d

Browse files
committed
Minor Fix
1 parent 99ff8ce commit 1efe64d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

pages/annotations/refinement-predicates.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ The `@Ghost` and `@StateSet` annotations are sugar for the `@RefinementPredicate
1616
| --- | --- |
1717
| `@Ghost("int size")` | `@RefinementPredicate("int size(ArrayList)")` |
1818
| `@Ghost("boolean open")` | `@RefinementPredicate("boolean open(InputStreamReader)")` |
19-
| `@StateSet({"open", "closed"})` | `@RefinementPredicate("int state1(File)")`<br>`state1(this) == 0 <=> empty(this)`<br>`state1(this) == 1 <=> full(this)` |
19+
| `@StateSet({"open", "closed"})` | `@RefinementPredicate("int state1(File)")`<br>`state1(this) == 0 <=> open(this)`<br>`state1(this) == 1 <=> closed(this)` |
2020

2121
In the current implementation, `@RefinementPredicate` is only supported on methods and constructors, but it is not currently scoped to the annotated method or constructor. Instead, is a global declaration that is available for the whole verification.
2222

0 commit comments

Comments
 (0)