Module dev.civl.mc
Package dev.civl.mc.predicate.IF

Interface FunctionalEquivalence

All Superinterfaces:
CIVLStatePredicate, dev.civl.gmc.StatePredicateIF<State>
public interface FunctionalEquivalence extends CIVLStatePredicate
A functional equivalence predicate contains a specification output, which is a set of pairs (pathcondition, output variable map), and is checked at the final state of the program. Given a specification and an implementation, the predicate is true if for every final state (p, o) of the implementation, there exists at least one entry (p', o') in the specification output such that p invalid input: '&'invalid input: '&' p' -> o=o'. Formally, suppose the specification output is {(p0, o0), (p1, o1), ...}, then the following predicate must be valid: p -> (p1 invalid input: '&'invalid input: '&' o=o1 || p2 invalid input: '&'invalid input: '&' o=o2 || ...).

  • Method Summary

    Modifier and Type
    Method
    Description
    Map<dev.civl.sarl.IF.expr.BooleanExpression,Set<Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression[]>>>
    specificationOutputs()
    The specification output of this predicate, which is a list of tuples of path condition and a map of (output) variables and their values.

    Methods inherited from interface dev.civl.mc.predicate.IF.CIVLStatePredicate

    getUnreportedViolation, getViolation, isAndPredicate

    Methods inherited from interface dev.civl.gmc.StatePredicateIF

    explanation, holdsAt

  • Method Details

    • specificationOutputs

      Map<dev.civl.sarl.IF.expr.BooleanExpression,Set<Pair<State,dev.civl.sarl.IF.expr.SymbolicExpression[]>>> specificationOutputs()
      The specification output of this predicate, which is a list of tuples of path condition and a map of (output) variables and their values.
      Returns: