Skip to content

Commit

Permalink
Merge pull request #2 from mernst/agora-javadoc
Browse files Browse the repository at this point in the history
Add Javadoc for some Agora invariants
  • Loading branch information
JuanCarlosAlonsoValenzuela authored Jul 22, 2023
2 parents 68aa5eb + 2900c7d commit a7d28c3
Show file tree
Hide file tree
Showing 16 changed files with 217 additions and 16 deletions.
1 change: 1 addition & 0 deletions java/daikon/inv/Joiner.java
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ public boolean isObviousDerived() {
return false;
}

@Pure
public @Nullable DiscardInfo isObviousImplied() {
return null;
}
Expand Down
15 changes: 14 additions & 1 deletion java/daikon/inv/unary/string/FixedLengthString.java
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
*/
public class FixedLengthString extends SingleString {

/** UID for serialization. */
static final long serialVersionUID = 20230704L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -38,17 +39,29 @@ public class FixedLengthString extends SingleString {
///
/// Required methods
///

/**
* Creates a new FixedLengthString.
*
* @param ppt the slice with the variable of interest
*/
private FixedLengthString(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype FixedLengthString. */
private @Prototype FixedLengthString() {
super();
}

/** The prototype invariant. */
private static @Prototype FixedLengthString proto = new @Prototype FixedLengthString();

// Returns the prototype invariant
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype FixedLengthString get_proto() {
return proto;
}
Expand Down
21 changes: 19 additions & 2 deletions java/daikon/inv/unary/string/IsEmail.java
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
* Email}.
*/
public class IsEmail extends SingleString {
/** UID for serialization. */
static final long serialVersionUID = 20230704L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -25,22 +26,38 @@ public class IsEmail extends SingleString {

private static Pattern pattern =
Pattern.compile(
"^(?:[a-z0-9!#$%&'*+/=?^_`{|}~-]+(?:\\.[a-z0-9!#$%&'*+/=?^_`{|}~-]+)*|\"(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21\\x23-\\x5b\\x5d-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])*\")@(?:(?:[a-z0-9](?:[a-z0-9-]*[a-z0-9])?\\.)+[a-z0-9](?:[a-z0-9-]*[a-z0-9])?|\\[(?:(?:25[0-5]|2[0-4][0-9]|[01]?[0-9][0-9]?)\\.){3}(?:25[0-5]|2[0-4][0-9]|[01]?[0-9]^[0-9]?|[a-z0-9-]*[a-z0-9]:(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21-\\x5a\\x53-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])+)\\])$");
// username
"^(?:[a-z0-9!#$%&'*+/=?^_`{|}~-]+(?:\\.[a-z0-9!#$%&'*+/=?^_`{|}~-]+)*|\"(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21\\x23-\\x5b\\x5d-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])*\")"
+ "@"
// domain
+ "(?:(?:[a-z0-9](?:[a-z0-9-]*[a-z0-9])?\\.)+[a-z0-9](?:[a-z0-9-]*[a-z0-9])?|\\[(?:(?:25[0-5]|2[0-4][0-9]|[01]?[0-9][0-9]?)\\.){3}(?:25[0-5]|2[0-4][0-9]|[01]?[0-9]^[0-9]?|[a-z0-9-]*[a-z0-9]:(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21-\\x5a\\x53-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])+)\\])$");

///
/// Required methods
///

/**
* Creates a new IsEmail.
*
* @param ppt the slice with the variable of interest
*/
private IsEmail(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype IsEmail. */
private @Prototype IsEmail() {
super();
}

/** The prototype invariant. */
private static @Prototype IsEmail proto = new @Prototype IsEmail();

// Returns the prototype invariant
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype IsEmail get_proto() {
return proto;
}
Expand Down
15 changes: 14 additions & 1 deletion java/daikon/inv/unary/string/IsNumeric.java
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@
* Numeric}.
*/
public class IsNumeric extends SingleString {
/** UID for serialization. */
static final long serialVersionUID = 20230704L;

private static Pattern pattern =
Expand All @@ -32,18 +33,30 @@ public class IsNumeric extends SingleString {
///
/// Required methods
///

/**
* Creates a new IsNumeric.
*
* @param ppt the slice with the variable of interest
*/
private IsNumeric(PptSlice ppt) {
super(ppt);
alwaysEmpty = true;
}

/** Creates a new prototype IsNumeric. */
private @Prototype IsNumeric() {
super();
}

/** The prototype invariant. */
private static @Prototype IsNumeric proto = new @Prototype IsNumeric();

// Returns the prototype invariant
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype IsNumeric get_proto() {
return proto;
}
Expand Down
16 changes: 15 additions & 1 deletion java/daikon/inv/unary/string/IsUrl.java
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@

/** Indicates that the value of a string variable is always a URL. Prints as {@code is Url}. */
public class IsUrl extends SingleString {

/** UID for serialization. */
static final long serialVersionUID = 20230704L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -27,17 +29,29 @@ public class IsUrl extends SingleString {
///
/// Required methods
///

/**
* Creates a new IsUrl.
*
* @param ppt the slice with the variable of interest
*/
private IsUrl(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype IsUrl. */
private @Prototype IsUrl() {
super();
}

/** The prototype invariant. */
private static @Prototype IsUrl proto = new @Prototype IsUrl();

// Returns the prototype invariant
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype IsUrl get_proto() {
return proto;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@
* All the elements of x have LENGTH=n}.
*/
public class SequenceFixedLengthString extends SingleStringSequence {

/** UID for serialization. */
static final long serialVersionUID = 20220423L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -27,18 +29,29 @@ public class SequenceFixedLengthString extends SingleStringSequence {
@Unused(when = Prototype.class)
private @Nullable Integer length = null;

/**
* Creates a new SequenceFixedLengthString.
*
* @param ppt the slice with the variable of interest
*/
protected SequenceFixedLengthString(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype SequenceFixedLengthString. */
protected @Prototype SequenceFixedLengthString() {
super();
}

/** The prototype invariant. */
private static @Prototype SequenceFixedLengthString proto =
new @Prototype SequenceFixedLengthString();

/** Returns the prototype invariant for CommonStringSequence. */
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype SequenceFixedLengthString get_proto() {
return proto;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@
* of x are emails}.
*/
public class SequenceStringElementsAreEmail extends SingleStringSequence {

/** UID for serialization. */
static final long serialVersionUID = 20230704L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -33,18 +35,29 @@ public class SequenceStringElementsAreEmail extends SingleStringSequence {
Pattern.compile(
"^(?:[a-z0-9!#$%&'*+/=?^_`{|}~-]+(?:\\.[a-z0-9!#$%&'*+/=?^_`{|}~-]+)*|\"(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21\\x23-\\x5b\\x5d-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])*\")@(?:(?:[a-z0-9](?:[a-z0-9-]*[a-z0-9])?\\.)+[a-z0-9](?:[a-z0-9-]*[a-z0-9])?|\\[(?:(?:25[0-5]|2[0-4][0-9]|[01]?[0-9][0-9]?)\\.){3}(?:25[0-5]|2[0-4][0-9]|[01]?[0-9]^[0-9]?|[a-z0-9-]*[a-z0-9]:(?:[\\x01-\\x08\\x0b\\x0c\\x0e-\\x1f\\x21-\\x5a\\x53-\\x7f]|\\\\[\\x01-\\x09\\x0b\\x0c\\x0e-\\x7f])+)\\])$");

/**
* Creates a new SequenceStringElementsAreEmail.
*
* @param ppt the slice with the variable of interest
*/
protected SequenceStringElementsAreEmail(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype SequenceStringElementsAreEmail. */
protected @Prototype SequenceStringElementsAreEmail() {
super();
}

/** The prototype invariant. */
private static @Prototype SequenceStringElementsAreEmail proto =
new @Prototype SequenceStringElementsAreEmail();

/** Returns the prototype invariant for CommonStringSequence. */
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype SequenceStringElementsAreEmail get_proto() {
return proto;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@
* Prints as {@code All the elements of x are Numeric}.
*/
public class SequenceStringElementsAreNumeric extends SingleStringSequence {

/** UID for serialization. */
static final long serialVersionUID = 20230704L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -32,18 +34,29 @@ public class SequenceStringElementsAreNumeric extends SingleStringSequence {
private static Pattern pattern =
Pattern.compile("^[+-]{0,1}(0|([1-9](\\d*|\\d{0,2}(,\\d{3})*)))?(\\.\\d*[0-9])?$");

/**
* Creates a new SequenceStringElementsAreNumeric.
*
* @param ppt the slice with the variable of interest
*/
protected SequenceStringElementsAreNumeric(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype SequenceStringElementsAreNumeric. */
protected @Prototype SequenceStringElementsAreNumeric() {
super();
}

/** The prototype invariant. */
private static @Prototype SequenceStringElementsAreNumeric proto =
new @Prototype SequenceStringElementsAreNumeric();

/** Returns the prototype invariant for CommonStringSequence. */
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype SequenceStringElementsAreNumeric get_proto() {
return proto;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,8 @@
* x are URLs}
*/
public class SequenceStringElementsAreUrl extends SingleStringSequence {

/** UID for serialization. */
static final long serialVersionUID = 20230704L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -33,18 +35,29 @@ public class SequenceStringElementsAreUrl extends SingleStringSequence {
Pattern.compile(
"^(?:(?:https?|ftp)://)(?:\\S+(?::\\S*)?@)?(?:(?!10(?:\\.\\d{1,3}){3})(?!127(?:\\.\\d{1,3}){3})(?!169\\.254(?:\\.\\d{1,3}){2})(?!192\\.168(?:\\.\\d{1,3}){2})(?!172\\.(?:1[6-9]|2\\d|3[0-1])(?:\\.\\d{1,3}){2})(?:[1-9]\\d?|1\\d\\d|2[01]\\d|22[0-3])(?:\\.(?:1?\\d{1,2}|2[0-4]\\d|25[0-5])){2}(?:\\.(?:[1-9]\\d?|1\\d\\d|2[0-4]\\d|25[0-4]))|(?:(?:[a-z\\x{00a1}-\\x{ffff}0-9]+-?)*[a-z\\x{00a1}-\\x{ffff}0-9]+)(?:\\.(?:[a-z\\x{00a1}-\\x{ffff}0-9]+-?)*[a-z\\x{00a1}-\\x{ffff}0-9]+)*(?:\\.(?:[a-z\\x{00a1}-\\x{ffff}]{2,})))(?::\\d{2,5})?(?:/[^\\s]*)?$");

/**
* Creates a new SequenceStringElementsAreUrl.
*
* @param ppt the slice with the variable of interest
*/
protected SequenceStringElementsAreUrl(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype SequenceStringElementsAreUrl. */
protected @Prototype SequenceStringElementsAreUrl() {
super();
}

/** The prototype invariant. */
private static @Prototype SequenceStringElementsAreUrl proto =
new @Prototype SequenceStringElementsAreUrl();

/** Returns the prototype invariant for CommonStringSequence. */
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype SequenceStringElementsAreUrl get_proto() {
return proto;
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@
* Prints as {@code All the elements of x are dates. Format: DD/MM/YYYY}.
*/
public class SequenceStringElementsAreDateDDMMYYYY extends SingleStringSequence {

/** UID for serialization. */
static final long serialVersionUID = 20230704L;

// Variables starting with dkconfig_ should only be set via the
Expand All @@ -42,18 +44,29 @@ public class SequenceStringElementsAreDateDDMMYYYY extends SingleStringSequence
Pattern.compile(
"^(?:0[1-9]|[12][0-9]|3[01])[-/.](?:0[1-9]|1[012])[-/.](?:19\\d{2}|20[01234][0-9]|2050)$");

/**
* Creates a new SequenceStringElementsAreDateDDMMYYYY.
*
* @param ppt the slice with the variable of interest
*/
protected SequenceStringElementsAreDateDDMMYYYY(PptSlice ppt) {
super(ppt);
}

/** Creates a new prototype SequenceStringElementsAreDateDDMMYYYY. */
protected @Prototype SequenceStringElementsAreDateDDMMYYYY() {
super();
}

/** The prototype invariant. */
private static @Prototype SequenceStringElementsAreDateDDMMYYYY proto =
new @Prototype SequenceStringElementsAreDateDDMMYYYY();

/** Returns the prototype invariant for CommonStringSequence. */
/**
* Returns the prototype invariant.
*
* @return the prototype invariant
*/
public static @Prototype SequenceStringElementsAreDateDDMMYYYY get_proto() {
return proto;
}
Expand Down
Loading

0 comments on commit a7d28c3

Please sign in to comment.