Skip to content

Preserve State in State Refinements without Postcondition#191

Open
rcosta358 wants to merge 2 commits intomainfrom
codex-issue-51
Open

Preserve State in State Refinements without Postcondition#191
rcosta358 wants to merge 2 commits intomainfrom
codex-issue-51

Conversation

@rcosta358
Copy link
Collaborator

@rcosta358 rcosta358 commented Mar 24, 2026

Closes #51.

Fixes a bug where @StateRefinement annotations with a from condition but no to condition were incorrectly treated as state transitions. This caused LiquidJava to weaken object state after calls that should only check a precondition, losing precise information needed by later calls.

Root cause

When a state refinement had from != null and to == null, the verifier created a post-state by copying from into to, which turned a pure state check into an actual transition. Fixed this by removing this part of the logic.

This means that, for example, a method that should only require x(this) > 0 could overwrite a more precise state such as x(this) == 2 with the weaker predicate x(this) > 0.

@rcosta358 rcosta358 self-assigned this Mar 24, 2026
@rcosta358 rcosta358 added the bug Something isn't working label Mar 24, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Unsolicited state transition

1 participant