Skip to content

Conversation

@rodrigomilisse
Copy link
Collaborator

Added basic support for boolean ghost variables. Only tested in trivial case

@alcides
Copy link
Collaborator

alcides commented Jul 14, 2025

Given how simple this is, I would consider writing more generic code that, for each type, returns the default value for the expression. If there is none, it fails with the current exception.

Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good! Just change the variables used in the test to make it more consistent with the variable names.
Also, the test should be in the testSuite, and make sure that it is run in CI (you can check if the filename is tested).

import liquidjava.specification.StateRefinement;

@Ghost("boolean opened")
@Ghost("boolean closed")
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is there a reason for having open and closed instead of just using opened and !opened?
If you want to test two different ghost variables do not use opposite ghost variables

closed = true;
}

@StateRefinement(from = "opened(this) && closed(this)")
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

related to the one before - it does not make sense to require open and closed at the same time

@CatarinaGamboa CatarinaGamboa mentioned this pull request Jul 27, 2025
@CatarinaGamboa
Copy link
Collaborator

@rodrigomilisse are you still planning on making changes here before we merge?

@rcosta358
Copy link
Collaborator

rcosta358 commented Oct 9, 2025

Also added support for double ghost variables

@rcosta358 rcosta358 requested a review from alcides October 22, 2025 11:02
@rcosta358 rcosta358 merged commit 69b00ca into main Oct 29, 2025
1 check passed
@rcosta358 rcosta358 deleted the ghost-boolean branch November 7, 2025 15:24
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.

6 participants