Repository navigation

Compute loop typestates as a fixpoint over iterations - #434

Merged

CatarinaGamboa merged 9 commits into

mainfrom

fix/427-loop-state-fixpoint

Nov 3, 2026

Merged

Compute loop typestates as a fixpoint over iterations#434
CatarinaGamboa merged 9 commits into
mainfrom
fix/427-loop-state-fixpoint

Commits on Oct 29, 2026
- Allow a state-changing call from a union of its entry states
  
  CatarinaGamboa
  and
  claude
  committed
  28cc19c
- Compute the typestate at a loop head as a fixpoint over its iterations
  
  CatarinaGamboa
  and
  claude
  committed
  11fc155
- Substitute call arguments in state predicates in one place
  
  CatarinaGamboa
  and
  claude
  committed
  5ea9c03
- Check each loop iteration from the same facts, and follow only recorded jumps
  
  CatarinaGamboa
  and
  claude
  committed
  f1fd0f5
- Recompute the metadata of a loop's elements in each check
  
  CatarinaGamboa
  and
  claude
  committed
  0149285
- Test the labelled-block if-join, and pin the loop jump fallback
  
  CatarinaGamboa
  and
  claude
  committed
  de8e96c
- Track the state of an object in none of the states of a set in loops
  
  CatarinaGamboa
  and
  claude
  committed
  606839d
- Simplify the loop typestate code
  
  CatarinaGamboa
  and
  claude
  committed
  cb1a49d
Commits on Oct 30, 2026
- Say in the StateSet Javadoc that an object may be in no state of a set
  
  CatarinaGamboa
  and
  claude
  committed
  a06f3c4