Module dev.civl.mc

Interface AccuracyAssumptionBuilder


public interface AccuracyAssumptionBuilder
An accuracy assumption builder provides logic for determining additional assumptions that should be added after an assumption involving an abstract function call.
  • Method Details

    • accuracyAssumptions

      Fragment accuracyAssumptions(Expression assumption, Scope scope)
      Analyze an assumption. If that assumption contains an abstract function call, use heuristics to come up with appropriate Taylor series expansions when possible. Return these as a fragment of code consisting of additional assumptions.
      Parameters:
      assumption - The expression being added to the path condition.
      scope - The scope containing the expression.
      Returns:
      A fragment (possibly empty) with assumptions relating to Taylor expansions of any abstract functions that are called within the assumption.