File tree Expand file tree Collapse file tree 8 files changed +85
-57
lines changed
liquidjava-example/src/main/java
liquidjava-verifier/src/main
java/liquidjava/rj_language/visitors Expand file tree Collapse file tree 8 files changed +85
-57
lines changed Original file line number Diff line number Diff line change 1+ package testSuite ;
2+
3+ import liquidjava .specification .Refinement ;
4+
5+ @ SuppressWarnings ("unused" )
6+ class CorrectEnumField {
7+ enum Color {
8+ Red , Green , Blue
9+ }
10+
11+ @ Refinement ("color != Color.Blue" )
12+ Color color ;
13+
14+ void setColor (@ Refinement ("c != Color.Blue" ) Color c ) {
15+ color = c ;
16+ }
17+
18+ public static void main (String [] args ) {
19+ CorrectEnumField cef = new CorrectEnumField ();
20+ cef .setColor (Color .Red ); // correct
21+ cef .setColor (Color .Green ); // correct
22+ }
23+ }
Original file line number Diff line number Diff line change 1+ package testSuite ;
2+
3+ import liquidjava .specification .Refinement ;
4+
5+ @ SuppressWarnings ("unused" )
6+ class CorrectEnumParam {
7+ enum Status {
8+ Active , Inactive , Pending
9+ }
10+
11+ Status process (@ Refinement ("status == Status.Inactive" ) Status status ) {
12+ return Status .Active ;
13+ }
14+
15+ public static void main (String [] args ) {
16+ CorrectEnumParam cep = new CorrectEnumParam ();
17+ cep .process (Status .Inactive ); // correct
18+ }
19+ }
Load Diff This file was deleted.
Original file line number Diff line number Diff line change @@ -19,15 +19,27 @@ public CorrectEnumUsage() {}
1919 public void setMode (Mode mode ) {
2020 this .mode = mode ;
2121 }
22+
23+ @ StateRefinement (from ="photoMode(this)" , to ="noMode(this)" )
24+ @ StateRefinement (from ="videoMode(this)" , to ="noMode(this)" )
25+ public void resetMode () {
26+ this .mode = null ;
27+ }
2228
2329 @ StateRefinement (from ="photoMode(this)" )
2430 public void takePhoto () {}
31+
32+ @ StateRefinement (from ="videoMode(this)" )
33+ public void takeVideo () {}
2534
2635
2736 public static void main (String [] args ) {
2837 // Correct
2938 CorrectEnumUsage st = new CorrectEnumUsage ();
30- st .setMode (Mode .Photo );
39+ st .setMode (Mode .Photo ); // noMode -> photoMode
3140 st .takePhoto ();
41+ st .resetMode (); // photoMode -> noMode
42+ st .setMode (Mode .Video ); // noMode -> videoMode
43+ st .takeVideo ();
3244 }
3345}
Original file line number Diff line number Diff line change 1+ // Refinement Error
2+ package testSuite ;
3+
4+ import liquidjava .specification .Refinement ;
5+
6+ @ SuppressWarnings ("unused" )
7+ class ErrorEnumNegation {
8+ enum Status {
9+ Active , Inactive , Pending
10+ }
11+
12+ void process (@ Refinement ("status != Status.Inactive" ) Status status ) {}
13+
14+ public static void main (String [] args ) {
15+ ErrorEnumNegation e = new ErrorEnumNegation ();
16+ e .process (Status .Active ); // correct
17+ e .process (Status .Inactive ); // error
18+ }
19+ }
Original file line number Diff line number Diff line change 22
33import liquidjava .specification .Refinement ;
44
5- public class EnumRefinementMessage {
5+ class EnumRefinementMessage {
66 enum Mode {
77 Photo , Video , Unknown
88 }
Original file line number Diff line number Diff line change @@ -38,13 +38,14 @@ literalExpression:
3838 | literal #lit
3939 | ID #var
4040 | functionCall #invocation
41- | enumCall #enum
41+ | enumerate #enum
4242 ;
4343
44- functionCall:
44+ functionCall :
4545 ghostCall
4646 | aliasCall
47- | dotCall;
47+ | dotCall
48+ ;
4849
4950dotCall :
5051 OBJECT_TYPE ' (' args? ' )'
@@ -56,8 +57,8 @@ ghostCall:
5657aliasCall :
5758 ID_UPPER ' (' args? ' )' ;
5859
59- enumCall :
60- ENUM_CALL ;
60+ enumerate :
61+ ENUM ;
6162
6263args : pred (' ,' pred)* ;
6364
@@ -98,7 +99,7 @@ ARITHOP : '+'|'*'|'/'|'%';//|'-';
9899
99100BOOL : ' true' | ' false' ;
100101ID_UPPER : ([A -Z ][a-zA-Z0 -9]*);
101- ENUM_CALL : [A -Z ][a-zA-Z0 -9_]* ' .' [A -Z ][a-zA-Z0 -9_]*;
102+ ENUM : [A -Z ][a-zA-Z0 -9_]* ' .' [A -Z ][a-zA-Z0 -9_]*;
102103OBJECT_TYPE :
103104 (([a-zA-Z ][a-zA-Z0 -9]+) (' .' [a-zA-Z ][a-zA-Z0 -9]*)+);
104105ID : ' #' *[a-zA-Z_ ][a-zA-Z0 -9_#]*;
Original file line number Diff line number Diff line change @@ -239,11 +239,9 @@ private List<Expression> getArgs(ArgsContext args) throws LJError {
239239 }
240240
241241 private Enumerate enumCreate (EnumContext enumContext ) {
242- String enumText = enumContext .enumCall ().getText ();
243- int lastDot = enumText .lastIndexOf ('.' );
244- String enumTypeName = enumText .substring (0 , lastDot );
245- String enumConstName = enumText .substring (lastDot + 1 );
246- return new Enumerate (enumTypeName , enumConstName );
242+ String enumText = enumContext .enumerate ().getText ();
243+ String [] parts = enumText .split ("\\ ." );
244+ return new Enumerate (parts [0 ], parts [1 ]);
247245 }
248246
249247 private Expression literalCreate (LiteralContext literalContext ) throws LJError {
You can’t perform that action at this time.
0 commit comments