Skip to content

Conversation

@Pichers
Copy link
Collaborator

@Pichers Pichers commented Jun 16, 2025

Description

Added a Class Level Map for the refined classes and the analysis functions in a new External Refinement First Pass to populate them.
The @ExternalRefinementsFor() annotation was added, based on the one in the LiquidJava repo.
The TypeChecker was altered to accommodate these additions.
This improvements do not yet accommodate return type annotations.

Example

Support for refinements like:

@ExternalRefinementsFor("java.util.ArrayList")
public interface ArrayListRefinements<E> {

    public void ArrayList();

    public void add(@Free E e);

    public boolean contains(@Free Object o);
}

Related Issue

#5

Type of change

  • Bug fix
  • New feature
  • Documentation update
  • Code refactoring

How Has This Been Tested?

Tests were added that analyse both correct and incorrect cases, not giving any unexpected results

@Pichers Pichers requested a review from CatarinaGamboa June 24, 2025 15:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants