Record Class FunctionSummary.RequirePredicate

java.lang.Object
java.lang.Record
org.ek9lang.compiler.symbolic.FunctionSummary.RequirePredicate
Record Components:
paramIndex - the 0-based position of the constrained parameter in the callee's signature
paramName - the parameter's name (for readability / caller-side matching)
op - the normalised relational operator (<, <=, >, >=, ==, <>)
literal - the integer literal the parameter is compared against
Enclosing class:
FunctionSummary
public static record FunctionSummary.RequirePredicate(int paramIndex, String paramName, String op, long literal) extends Record
A single require precondition: param OP literal, keyed to the parameter's position so a call site can map it onto the matching argument.

  • Constructor Summary

    Constructors
    Constructor
    Description
    RequirePredicate(int paramIndex, String paramName, String op, long literal)
    Creates an instance of a RequirePredicate record class.

  • Method Summary

    Modifier and Type
    Method
    Description
    final boolean
    equals(Object o)
    Indicates whether some other object is "equal to" this one.
    boolean
    excludesZero()
    Whether this precondition guarantees the parameter is non-zero — so a division by that parameter, dominated by this require, is discharged (cannot divide by zero).
    final int
    hashCode()
    Returns a hash code value for this object.
    long
    literal()
    Returns the value of the literal record component.
    String
    op()
    Returns the value of the op record component.
    int
    paramIndex()
    Returns the value of the paramIndex record component.
    String
    paramName()
    Returns the value of the paramName record component.
    final String
    toString()
    Returns a string representation of this record class.
    long
    violatingArgValue()
    The argument value that violates this precondition — the boundary at (or just past) the literal, depending on the operator.

    Methods inherited from class Object

    clone, finalize, getClass, notify, notifyAll, wait, wait, wait

  • Constructor Details

    • RequirePredicate

      public RequirePredicate(int paramIndex, String paramName, String op, long literal)
      Creates an instance of a RequirePredicate record class.
      Parameters:
      paramIndex - the value for the paramIndex record component
      paramName - the value for the paramName record component
      op - the value for the op record component
      literal - the value for the literal record component

  • Method Details

    • excludesZero

      public boolean excludesZero()
      Whether this precondition guarantees the parameter is non-zero — so a division by that parameter, dominated by this require, is discharged (cannot divide by zero).

    • violatingArgValue

      public long violatingArgValue()
      The argument value that violates this precondition — the boundary at (or just past) the literal, depending on the operator. Feeding this back through a caller's argument transform yields the caller input that panics. E.g. require x <> 0 is violated by x = 0.

    • toString

      public final String toString()
      Returns a string representation of this record class. The representation contains the name of the class, followed by the name and value of each of the record components.
      Specified by:
      toString in class Record
      Returns:
      a string representation of this object

    • hashCode

      public final int hashCode()
      Returns a hash code value for this object. The value is derived from the hash code of each of the record components.
      Specified by:
      hashCode in class Record
      Returns:
      a hash code value for this object

    • equals

      public final boolean equals(Object o)
      Indicates whether some other object is "equal to" this one. The objects are equal if the other object is of the same class and if all the record components are equal. Reference components are compared with Objects::equals(Object,Object); primitive components are compared with the compare method from their corresponding wrapper classes.
      Specified by:
      equals in class Record
      Parameters:
      o - the object with which to compare
      Returns:
      true if this object is the same as the o argument; false otherwise.

    • paramIndex

      public int paramIndex()
      Returns the value of the paramIndex record component.
      Returns:
      the value of the paramIndex record component

    • paramName

      public String paramName()
      Returns the value of the paramName record component.
      Returns:
      the value of the paramName record component

    • op

      public String op()
      Returns the value of the op record component.
      Returns:
      the value of the op record component

    • literal

      public long literal()
      Returns the value of the literal record component.
      Returns:
      the value of the literal record component