Repository navigation
In-source return refinement _ == true --> s(this) binds this to the return value (Argument Mismatch) #442
Description
A boolean method that reveals a state when it returns true, @Refinement("_ == true --> b(this)"), fails when the class is annotated in its own source. The same form verifies in an @ExternalRefinementsFor spec.
Reproducer (one file; run the verifier on it):
import liquidjava.specification.Refinement;
import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;
@StateSet({"a", "b"})
class Edit {
@StateRefinement(to = "a(this)")
public Edit() {}
@StateRefinement(to = "b(this)")
public void finish() {}
@Refinement("_ == true --> b(this)")
public boolean isDone() { return true; }
@StateRefinement(from = "b(this)")
public void needsB() {}
}
public class Main {
static void use(Edit e) {
if (e.isDone()) e.needsB(); // a true answer says b
}
public static void main(String[] args) { Edit e = new Edit(); e.finish(); use(e); }
}Found on main @ f7f366c (also on 1a506fe):
Argument Mismatch Error: Argument '#ret_6' and its respective parameter of ghost 'Edit.state1' types are incompatible: expected Edit, got boolean
19 | public boolean isDone() { return true; }
this in the return refinement seems to be bound to the return value (#ret_6) instead of the receiver.
Expected: the program verifies, as it does when the same refinements are written in an external spec. For example, this one verifies:
@ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
@StateSet({"done", "undone"})
public interface EditRefinements {
@StateRefinement(to = "done(this)") void AbstractUndoableEdit();
@Refinement("_ == true --> done(this)") boolean canUndo();
@StateRefinement(from = "done(this)", to = "undone(this)") void undo();
}
// client: static void use(AbstractUndoableEdit e) { if (e.canUndo()) e.undo(); }Found while cataloguing spec forms for co-specification; the reproducers are probes V11 (in-source) and V21 (external) there. Low priority: external specs, the main use, work.
Activity