Skip to content

Commit fac2b6d

Browse files
committed
Minor Fixes
1 parent 06cf651 commit fac2b6d

2 files changed

Lines changed: 1 addition & 2 deletions

File tree

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ import liquidjava.specification.*;
1616
@ExternalRefinementsFor("java.util.Stack")
1717
@Ghost("int size")
1818
public interface StackRefinements<E> {
19-
2019
@StateRefinement(to="size() == 0")
2120
public void Stack();
2221

reference/refinements.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ public class RefinementExamples {
3333

3434
## Predicate Syntax
3535

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.
36+
Refinement predicates use a language similar to Java, where you can write boolean expressions using comparisons, logical connectives, arithmetic operators, conditional expressions, and calls to ghosts or aliases, which we cover in later sections.
3737

3838
| Form | Syntax | Example |
3939
| --- | --- | --- |

0 commit comments

Comments
 (0)