Package daikon

Class VarInfoName.QuantHelper

  • Enclosing class:
    VarInfoName
    public static class VarInfoName.QuantHelper
extends Object
    Helper for writing parts of quantification expressions. Formatting methods in invariants call the formatting methods in this class to get commonly-used parts, like how universal quanitifiers look in the different formatting schemes.

    • Field Detail

      • debug

        public static final Logger debug
        Debug tracer.

    • Method Detail

      • replace

        public static VarInfoName[] replace​(VarInfoName root,
                                    VarInfoName needy,
                                    VarInfoName index)
        Replaces a needy (unquantified term) with its subscripted equivalent, using the given index variable.
        Parameters:
        root - the root of the expression to be modified. Substitution occurs only in the subtree reachable from root.
        needy - the term to be subscripted (must be of type Elements or Slice)
        index - the variable to place in the subscript
        Returns:
        a 3-element array consisting of the new root, the lower bound for the index (inclusive), and the upper bound for the index (inclusive), in that order

      • selectNth

        public static VarInfoName selectNth​(VarInfoName root,
                                    @Nullable VarInfoName index_base,
                                    int index_off)
        Assuming that root is a sequence, return a VarInfoName representing the (index_base+index_off)-th element of that sequence. index_base may be null, to represent 0.

      • selectNth

        public static VarInfoName selectNth​(VarInfoName root,
                                    String index_base,
                                    boolean free,
                                    int index_off)
        Assuming that root is a sequence, return a VarInfoName representing the (index_base+index_off)-th element of that sequence. index_base may be null, to represent 0.

      • format_esc

        public static String[] format_esc​(VarInfoName[] roots)
        Given a list of roots, return a String array where the first element is a ESC-style quantification over newly-introduced bound variables, the last element is a closer, and the other elements are esc-named strings for the provided roots (with sequences subscripted by one of the new bound variables).

      • simplifyNameAndBounds

        public static String[] simplifyNameAndBounds​(VarInfoName name)
        Given a list of roots, return a String array where the first element is a JML-style quantification over newly-introduced bound variables, the last element is a closer, and the other elements are jml-named strings for the provided roots (with sequenced subscripted by one of the new bound variables).

      • format_simplify

        public static String[] format_simplify​(VarInfoName[] roots)
        Given a list of roots, return a String array where the first element is a simplify-style quantification over newly-introduced bound variables, the last element is a closer, and the other elements are simplify-named strings for the provided roots (with sequences subscripted by one of the new bound variables).

        If elementwise is true, include the additional contraint that the indices (there must be exactly two in this case) refer to corresponding positions. If adjacent is true, include the additional constraint that the second index be one more than the first. If distinct is true, include the constraint that the two indices are different. If includeIndex is true, return additional strings, after the roots but before the closer, with the names of the index variables.

      • format_simplify

        public static String[] format_simplify​(VarInfoName[] roots,
                                       boolean elementwise,
                                       boolean adjacent,
                                       boolean distinct,
                                       boolean includeIndex)

      • format_java_style

        protected static String[] format_java_style​(VarInfoName[] roots,
                                            OutputFormat format)
        Given a list of roots, return a String array where the first element is a Java-style quantification over newly-introduced bound variables, the last element is a closer, and the other elements are java-named strings for the provided roots (with sequences subscripted by one of the new bound variables).

      • quant_increment

        protected static String quant_increment​(VarInfoName idx,
                                        int i,
                                        OutputFormat format)
        This function creates a string that represents how to increment the variables involved in quantification. Since the increment is not stated explicitly in the JML and ESC formats this function merely returns an empty string for those formats.

      • quant_format_forall

        protected static String quant_format_forall​(OutputFormat format)
        This function returns a string representing how to format a forall statement in a given output mode.

      • quant_format_exists

        protected static String quant_format_exists​(OutputFormat format)
        This function returns a string representing how to format an exists statement in a given output mode.

      • quant_separator1

        protected static String quant_separator1​(OutputFormat format)
        This function returns a string representing how to format the first seperation in the quantification, that is, the one between the intial condition and the execution condition.

      • quant_separator2

        protected static String quant_separator2​(OutputFormat format)
        This function returns a string representing how to format the second seperation in the quantification, that is, the one between the execution condition and the assertion.

      • quant_step_terminator

        protected static String quant_step_terminator​(OutputFormat format)
        This function returns a string representing how to format the final seperation in the quantification, that is, the one between the assertion and any closing symbols.