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
boolean	admits(long value)	Whether value SATISFIES this precondition — the complement of violatingArgValue(), and the primitive a generator needs to keep an argument out of a test that could only ever Panic.
long	boundaryAdmittedValue()	The admitted value sitting hard against the boundary — the in-contract edge worth driving.
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).

admits

public boolean admits(long value)

Whether value SATISFIES this precondition — the complement of violatingArgValue(), and the primitive a generator needs to keep an argument out of a test that could only ever Panic.

🔑 An unmodelled operator admits everything. This analysis is one-sided by design (McMinn et al.): it may RETAIN a value it could have excluded, and must NEVER exclude one it cannot prove excluded. Over-retention costs a redundant test; over-exclusion silently deletes the case that would have found the bug.

Parameters:

value - the candidate argument

Returns:

true when the precondition holds for value, or the operator is not modelled

boundaryAdmittedValue

public long boundaryAdmittedValue()

The admitted value sitting hard against the boundary — the in-contract edge worth driving. require n > 0 yields 1; require n >= 18 yields 18.

This is the DECLARED half of boundary extraction (SPEC-test-data-generation.md §2, analysis D). Its out-of-contract twin is violatingArgValue(), which belongs in a Panic-asserting test rather than an ordinary one.

Returns:

the closest argument value that satisfies this precondition

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