Skip to content

Add Hints for Unconstrained Refinements #288

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
rcosta358 wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Add Hints for Unconstrained Refinements #288

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b7dba4a
Add Hint for Unconstrained Refinements
rcosta358 Aug 27, 2026
9986b21
Update State Refinement Hint
rcosta358 Aug 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 12 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
package testSuite;

import liquidjava.specification.Refinement;

public class ErrorUnconstrainedRefinement {

private static void requirePositive(@Refinement("_ > 0") int value) {}

public static void check(int value) {
requirePositive(value); // Refinement Error
}
}
15 changes: 15 additions & 0 deletions liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
package testSuite;

import liquidjava.specification.Ghost;
import liquidjava.specification.StateRefinement;

@Ghost("boolean ready")
public class ErrorUnconstrainedStateRefinement {

@StateRefinement(from = "ready(this)")
public void run() {}

public static void check(ErrorUnconstrainedStateRefinement value) {
value.run(); // State Refinement Error
}
}
15 changes: 15 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ public class LJDiagnostic extends RuntimeException {
private String file;
private SourcePosition position;
private String hint;
private String counterexample;
private static final String PIPE = " | ";

public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
Expand Down Expand Up @@ -43,6 +44,10 @@ public String getHint() {
return hint;
}

public String getCounterexampleStr() {
return counterexample;
}

public SourcePosition getPosition() {
return position;
}
Expand Down Expand Up @@ -70,6 +75,10 @@ public void setHint(String hint) {
this.hint = hint;
}

public void setCounterexampleStr(String counterexample) {
this.counterexample = counterexample;
}

@Override
public String toString() {
StringBuilder sb = new StringBuilder();
Expand All @@ -84,6 +93,12 @@ public String toString() {
sb.append(snippet);
}

// counterexample
String counterexample = getCounterexampleStr();
if (counterexample != null && !counterexample.isBlank()) {
sb.append(" --> ").append(String.join("\n ", counterexample.split("\n"))).append("\n");
}

// hint
String hint = getHint();
if (hint != null && !hint.isBlank()) {
Expand Down
21 changes: 10 additions & 11 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@
import liquidjava.utils.Pair;
import spoon.reflect.cu.SourcePosition;

import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;

/**
* Error indicating that a refinement constraint either was violated or cannot be proven
*
Expand All @@ -37,24 +39,21 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
this.found = found;
this.counterexample = filterCounterexample(counterexample);
this.declarationPosition = declarationPosition;
if (!this.counterexample.isEmpty()) {
String counterexampleString = this.counterexample.assignments().stream()
.map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
.collect(Collectors.joining(" && "));
setCounterexampleStr("Counterexample: " + counterexampleString);
}
if (isTrue(found.getImplication().toPredicate().getExpression()))
setHint("Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.");
}

@Override
public SourcePosition getDeclarationPosition() {
return declarationPosition;
}

@Override
public String getHint() {
if (counterexample.isEmpty())
return null;

String counterexampleString = counterexample.assignments().stream()
.map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
.collect(Collectors.joining(" && "));
return "Counterexample: " + counterexampleString;
}

public Counterexample getCounterexample() {
return counterexample;
}
Expand Down
4 changes: 4 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
package liquidjava.diagnostics.errors;

import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;

import liquidjava.diagnostics.TranslationTable;
import liquidjava.processor.VCImplication;
import liquidjava.rj_language.Predicate;
Expand Down Expand Up @@ -27,6 +29,8 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
this.declarationPosition = declarationPosition;
this.expected = expected;
this.found = found;
if (isTrue(found.getImplication().toPredicate().getExpression()))
setHint("No state information is known for this object. Make sure its state is initialized and available at this point.");
}

@Override
Expand Down
Loading