Interface contracts help improve software quality through their support for the explicit definition and enforcement of expected behaviors at call boundaries. Quality, as defined by the Institute of Electrical and Electronics Engineers (IEEE) [], is the degree to which a system, component, or process meets its specifications, needs, or expectations. Therefore, interface contracts may be used to address quality in terms of defining the expected behaviors of callers (or clients) and callee’s (i. e., servers or implementations) of methods. Specifications, in the form of executable assertions, have a long history of adding value to the software development process by helping ensure software is implemented and used correctly. Parnas [] advocated machine testable, implementation-neutral component specifications in 1971. Thirty years later, Baudry et al. [] found components with high encapsulation and well-defined, contractually-specified interfaces to be more effective at improving the quality of systems than implementation-dependent assertions used for defensive programming. Babel supports both the optional specification and automated enforcement of interface contracts.
Executable, programming language-neutral constraints on the (public) methods of interfaces and classes are supported in SIDL. These specifications define the software behaviors required and expected at call boundaries regardless of the programming language(s) used to implement the methods. The associated constraints may be checked at runtime through a variety of enforcement options intended for different phases of the software life cycle.
Interface contracts consist of one or more clauses defining expected behaviors at method call boundaries. The behaviors are specified through assertions, which may include built-in or user-defined function calls. An example for calculating the sum of two vectors1 is shown below. All callers of this method are required to provide two one-dimensional, SIDL arrays of the same size and, assuming the preconditions are satisfied, all implementations are expected to ensure they return a non-null, one-dimensional array of the same size (as the first SIDL array). The specification includes the invocation of two built-in functions: dimen and size. Violations of an assertion within a clause results in the raising of a clause-specific exception; namely, sidl.PreViolation if the caller violates the contract or sidl.PostViolation if the implementation violates the contract. Hence, this example defines constraints that are to hold immediately prior to (or preconditions on) and immediately upon return from (or postconditions of) executing the vuSum method defined in the Utils class within the vect package.
| package vect version 1.0 { class Utils { /* ... */ /** * Return the sum of the specified vectors. */ static array<double> vuSum(in array<double> u, in array<double> v) throws sidl.PreViolation, sidl.PostViolation; require not_null_u: u != null; u_is_1d : dimen(u) == 1; not_null_v: v != null; v_is_1d : dimen(v) == 1; same_size: size(u) == size(v); ensure no_side_effects : is pure; result_not_null: result != null; result_is_1d : dimen(result) == 1; result_correct_size: size(result) == size(u); } /* ... */ } |
The remainder of this section elaborates on the contents of contract clauses. Clauses consist of assertion expressions specified using an Eiffel-inspired syntax. SIDL expressions may contain basic and advanced operations as well as built-in and user-defined function calls. The detection of contract violations result in the automatic raising of clause-specific exceptions.
There are three types of contract clauses associated with interfaces: preconditions, postconditions, and class invariants. Preconditions declare constraints on invocation of a method while postconditions constrain its effects. Class invariants specify properties unchanged throughout the life of an instance of a class so apply to all of the defined methods. While all three clause types share a common format for specifying these constraints2, their location with the specification varies.
As introduced in Section 6.5, the format of a contract clause starts with a clause keyword followed by one or more assertion expressions. The syntax was borrowed from the classic Eiffel [] clauses established by Bertrand Meyer. The figure below shows the SIDL format, including all supported clause types. Each expression may be preceded by a label. If thoughtfully written, the label can provide a succinct “description” of the purpose of the assertion to aid debugging, since labels are automatically included in the exception message of a violated contract clause. Expressions are described in Section 21.2.2.
| <require | ensure | invariant> [label-1:] <assertion-expression-1>; [[label-2:] <assertion-expression-2>; ... [label-n:] <assertion-expression-n>;] |
Since preconditions and postconditions are associated with specific methods, their definitions are optional extensions in SIDL. The figure below shows the basic structure of a SIDL method specification, including the relative locations of the preconditions, or require, and postconditions, or ensure, clauses. When contract clauses are added to the specification, each method’s throws clause must explicitly list the appropriate contract clause violation exception3. Exceptions are described in Section 21.2.3.
| [<type>] <identifier> ( [<parameters>] ) [throws <exception>]; [require <contract-clause-expressions>] [ensure <contract-clause-expressions>] |
Class invariants apply to all specified methods associated with a class so, instead of requiring them to be defined for each method, the invariant clause is provided. The clause, which may be specified for an interface or class, must appear before method definitions start. The basic structures of interface and class specifications, to include the invariant clause, appear below.
| [ abstract ] class <name> [ extends <scoped-class-name> ] [ implements-all <scoped-interface-name-list> ] { [ invariant <contract-clause-expressions> ] [ abstract | final | static ] <method-1> [ [ abstract | final | static ] <method-2> ... [ abstract | final | static ] <method-n> ] } [;] interface <name> [ extends <scoped-interface-name-list> ] { [ invariant <contract-clause-expressions> ] <method-1> [ <method-2> ... <method-n> ] } [;] |
SIDL contract clauses can be inherited. However, all assertion expressions — directly defined and inherited — are aggregated on a clause basis and checks built by essentially and’ing them. This results in effectively strengthening (i. e., applying and then) to the inherited clauses; rather, than the proper notion of weakening (i. e., applying or else to) inherited precondition clauses. No optimization is performed on the resulting checks either. The interested reader should consult [] and [] for more information on (proper) contract inheritance behavior.
Hence, SIDL’s interface contract specifications are based on three types of contract clauses: preconditions, postconditions, and class invariants. While all three share a common basic format — keyword followed by a list of assertion expressions — they appear in different locations within the specification. Specifically, postconditions follow preconditions within the definition of a method; while class invariants are specified before methods in class and interface definitions.
Table 21.1: Operators available for use in SIDL assertion expressions.
OPERATOR(S) DESCRIPTION <, <= Is less than, Is less than or equal to ==, != Is equal to, Is not equal to >, >= Is greater than, Is greater than or equal to +, - Addition, Subtraction *, / Multiplication, Division ** Power and Logical and iff If and only if implies Implies is Is (paired with the pure keyword) mod Modulo not Is not or Inclusive or rem Remainder xor Exclusive or
Assertion expressions represent properties that must be true at the execution point corresponding to their containing contract clause. These expressions are composed of operators and operands. Individual operands may take the form of arguments, results, constants, or function calls. Arguments and results make sense only for clauses associated with specific methods (i. e., preconditions and postconditions). Constant values and function calls may be specified in any contract clause.
Basic expression syntax is supported, including the use of parentheses to indicate precedence. Expressions may involve unary or binary operators. They may be as basic as a simple comparison (e. g. u != null) or involve multiple comparisons (e. g. (u != null) implies (size(u) >= 0)4). Regardless of the number of sub-expressions, every assertion expression must evaluate to a boolean result.
SIDL assertion expression operators include those operators available in most common programming languages, as well as some advanced operators, such as iff (for if and only if) and implies. Table 21.1 provides a complete list. Advanced operations, for universal and existential quantification, are also supported, though through built-in functions described later in this section. The associated operands may take the form of arguments, results, constant values, and method calls.
Precondition and postcondition clauses may include constraints on the arguments and results of the associated method. Arguments are referenced using their names as specified in the method’s parameter list. The method’s result, which is not named in the specification, is represented in the expression by the generic result keyword, which takes on the method’s return type.
Table 21.2: Special keywords available for use in SIDL assertion expressions.
KEYWORD MEANING false False null Null reference pure Side effect-free result Method result true True
Constants, such as boolean and numeric values, are also supported. Table 21.2, which lists all of the keywords allowed in SIDL assertion expressions, includes recognized boolean and pointer value representations. The table also includes two special keywords: pure and result. The former, when paired with the is operator, as in is pure, represents a non-executable postcondition annotation used to indicate implementations of the method should be side effect-free. This property is necessary so the method (or function) can be safely used in an interface contract; however, there is no support in the toolkit for statically analyzing source code (in any of the supported programming languages) to ensure the property is true for implementations of the interface. As mentioned previously, result represents the value returned by the associated method.
Function calls are supported within contract clauses to enable the definition of richer constraints. They enable restrictions on object properties, which are not visible in SIDL, and (interface- or class-specific) logic enhancing contract expressiveness. The functions may be built-in or in scope, user-defined methods.
Table 21.3: Built-in SIDL interface contract functions, where expr can be one of: u r v, u r n, and n r v with u, v ∈ SIDL arrays, n ∈ Numbers, and r ∈ {<, >, <=, >=, ==, !=}. The relation u r v is equivalent to ∀ i ∈ 0 .. (size(u)−1), u[i] r v[i]; u r n to ∀ i ∈ 0 .. (size(u)−1), u[i] r n; and n r v to ∀ i ∈ 0 .. (size(v)−1), n r u[i].
FUNCTION RETURNS COMPLEXITY dimen(u) Dimension of array u. O(1) irange(x, nlow, nhigh) True if x falls within the integer range of nlow..nhigh. O(1) lower(u, d) Lower index of the dth dimension of array u. O(1) nearEqual(x, y, t) True if real values x and y are within the specified tolerance, t, of being equal. O(1) range(x, rlow, rhigh, t) True if the real value x falls within the specified tolerance, t, of the range rlow..rhigh. O(1) size(u) Allocated size of array u. O(1) stride(u, d) Stride of the dth dimension of array u. O(1) upper(u, d) Upper index of the dth dimension of array u. O(1) all(expr) True if the expression expr evaluates to true for each element in the specified array(s). For example, all(u < v) returns true if the value of each element in array u is less than the value of the corresponding element in array v. O(n) any(expr) True if at least one element in the specified array(s) satisfies the expression expr. For example, any(u = 0) returns true upon encountering the first element in array u whose value equals zero but returns false if none of the elements have values equal zero. O(n) count(expr) The total number of array elements satisfying the expression expr. O(n) irange(u, nlow, nhigh) True if all elements in the array, u, fall within the integer range nlow..nhigh. O(n) max(u) The maximum of the values of the elements in array u. O(n) min(u) The minimum of the values of the elements in array u. O(n) nearEqual(u, v, t) True if the corresponding elements in arrays u and v are within the specified tolerance, t, of being equal. O(n) none(expr) True if none of the elements in the specified array(s) satisfies the expression expr. For example, none(u >= 0.0) returns true if none of the elements of array u have values greater than or equal to 0.0. O(n) nonDecr(u) True if the values of the elements in array u are in non-decreasing order. O(n) nonIncr(u) True if the values of the elements in array u are in non-increasing order. O(n) range(u, rlow, rhigh, t) True if all elements in array u fall within the specified tolerance, t, of rlow .. rhigh. O(n) sum(u) Returns the total of the values of all elements in array u. O(n)
Built-in functions, described in Table 21.3, provide scalar and SIDL array features, with the latter enabling universal (e. g. all) and existential (e. g. any) quantification. Array property and simple numeric value comparator functions operate in constant-time. Other array-based operations, such as existential and universal quantifiers, are linear in the size of the arrays. Their complexity is mentioned here because it is relevant to some of the experimental enforcement policies described in Section 21.3.
Allowing the specification of user-defined functions within contract clauses poses a risk in that implementors may erroneously come to depend on them — and their side effects — for proper implementation behavior. This is a mistake. The runtime enforcement of interface contracts is optional and, therefore, cannot be relied upon for correct functionality. This is why Babel requires the contract of user-defined functions intended or able to be used in the contract of another method to include the is pure postcondition annotation described previously.
In summary, SIDL contract clauses contain a list of one or more simple or compound expressions, each evaluating to a boolean value. Expressions may contain any of twenty built-in, basic or advanced operators; method arguments and results (only in precondition and postcondition clauses); special keywords; boolean and numeric constants; twenty built-in scalar and SIDL array functions; and in scope, user-defined functions. While there is a potential danger associated with allowing user-defined functions within contract clauses, the ability is supported to enable richer constraints and provide a mechanism for identifying and prototyping potential domain-specific contract features.
Enforcement is performed on a contract clause basis so, if an assertion does not hold, a clause-specific exception is automatically raised. That is, the sidl.PreViolation exception is raised when preconditions are violated; sidl.PostViolation raised for postcondition violations; and sidl.InvViolation for invariants violations. The exceptions, as defined in sidl.sidl, are shown below. The label, if any, of the associated assertion expression is included in the exception message; therefore, meaningful labels can aid testing and debugging.
| /** * <code>PreViolation</code> indicates an assertion within a precondition * clause of the interface contract has been violated. */ class PreViolation extends SIDLException implements RuntimeException {} /** * <code>PostViolation</code> indicates an assertion within a postcondition * clause of the interface contract has been violated. */ class PostViolation extends SIDLException implements RuntimeException {} /** * <code>InvViolation</code> indicates an assertion within a invariant * clause of the interface contract has been violated. */ class InvViolation extends SIDLException implements RuntimeException { } |
Interface contract enforcement is based on a global policy set at runtime. The policy establishes the contract clauses of interest and the frequency at which they should be checked. These two options support traditional contract/assertion enforcement as well as experimental strategies. The policy also supports enforcement tracing, though a discussion of this feature is provided separately in Section 21.3.4.
The enforcement policy should reflect the goals of the run which, as mentioned in Section 6.5, are often tied to the phase in the software’s life cycle. Available enforcement options range from traditional to experimental, with the former focused on aiding testing, debugging, and deployment. Some experimental options support a reduced level of enforcement intended for performance-contrained environments, while others are for gathering data to facilitate gaining insights into the nature of interface contract enforcement.
The SIDL specification of the enforcement policy is:
| /** * <code>EnfPolicy</code> maintains the current interface * contract enforcement policy. */ class EnfPolicy { /** * Sets the enforcement policy to always check the specified * type(s) of contracts. This is equivalent to calling * setPolicy() with ALWAYS as the enforcement frequency * and the specified (or default) contract class. * * @param contractClass Contract classification * [Default = ALLCLASSES] * @param clearStats TRUE if enforcement statistics are to be * cleared; FALSE otherwise. */ static void setEnforceAll(in ContractClass contractClass, in bool clearStats); /** * Sets the policy options to disable all contract enforcement. * This is equivalent to calling setPolicy() with NEVER as the * enforcement frequency. * * @param clearStats TRUE if enforcement statistics are to be * cleared; FALSE otherwise. */ static void setEnforceNone(in bool clearStats); /** * Sets enforcement policy and options. This method should be * invoked directly to avoid the default enforcement behavior. * * @param contractClass Contract classification * [Default = ALLCLASSES] * @param enforceFreq Enforcement frequency * [Default = ALWAYS] * @param interval Sampling interval representing the * period (for PERIODIC) or maximum * random number/window (for RANDOM) * [Default = 0 if negative specified] * @param overheadLimit Limit on performance overhead [0.0 .. 1.0) * [Default = 0.0 (or 0%) if negative] * @param appAvgPerCall Average extra, application-specific * execution time, normalized by calls * to annotated methods * [Default = 0.0 if negative] * @param annealLimit Limit on simulated annealing function * to ensure its termination * (0.0 .. 2.72] * [Default = 2.72 if negative specified] * @param clearStats TRUE if enforcement statistics are to be * cleared; FALSE otherwise. */ static void setPolicy(in ContractClass contractClass, in EnforceFreq enforceFreq, in int interval, in double overheadLimit, in double appAvgPerCall, in double annealLimit, in bool clearStats); /** * Returns TRUE if contract enforcement is enabled; FALSE otherwise. */ static bool areEnforcing(); /** * Returns the contract classification policy option. */ static ContractClass getContractClass(); /** * Returns the enforcement frequency policy option. */ static EnforceFreq getEnforceFreq(); /** * Returns the interval for PERIODIC (i.e., the interval) or * RANDOM (i.e., the maximum random number). Returns 0 by default. */ static int getSamplingInterval(); /** * Returns the desired enforcement overhead limit for * performance-driven frequency options (i.e., ADAPTFIT, * ADAPTTIMING, and SIMANNEAL). Returns 0.0 by default. */ static double getOverheadLimit(); /** * Returns the average assumed execution time associated * with the program or application. Returns 0.0 by default. */ static double getAppAvgPerCall(); /** * Returns the annealing limit for SIMANNEAL enforcement * frequency option. Returns 0.0 by default. */ static double getAnnealLimit(); /** * Returns the name, or description, of the enforcement policy. * The caller is responsible for calling sidl_String_free() * on the name when done with it. * * @param useAbbrev TRUE if the abbreviated name is to be * returned. */ static string getPolicyName(in bool useAbbrev); /** * Prints statistics data to the file with the specified name. * The file is opened (for append) and closed on each call. * * @param filename Name of the file to which the statistics * data should be written. * @param header TRUE if the header line is to be printed * prior to the statistics line (for compressed * output only). * @param prefix String description for identifying information, * if any, intended to preceed the statistics * data. Useful for distinguishing between * different objects, for example. * @param compressed TRUE if the enforcer state is to be dumped * on a single line with semi-colon separators * between fields. */ static void dumpStats(in string filename, in bool header, in string prefix, in bool compressed); /** * Starts enforcement trace file generation. * * @param filename Name of the destination trace file. * @param traceLevel Level of trace timing and reporting required. * [Default = NONE] */ static void startTrace(in string filename, in EnfTraceLevel traceLevel); /** * Returns TRUE if contract enforcement tracing is enabled; * FALSE otherwise. */ static bool areTracing(); /** * Returns the name of the trace file. If one was not provided, * the default name is returned. */ static string getTraceFilename(); /** * Returns the level of enforcement tracing. */ static EnfTraceLevel getTraceLevel(); /** * Terminates enforcement trace file generation. Takes a final * timestamp and logs the remaining trace information. */ static void endTrace(); } |
This class provides the ability to set and query enforcement options and statistics, as well as enforcement tracing. Two options establish the enforcement policy: contract clause classifications and enforcement frequency. Classification options identify either the clause or characteristics of the assertions within clauses. Some classification options reflect traditional contract enforcement strategies while others enable data gathering. Enforcement frequency options distinguish between traditional enforcement — where all associated contract clauses are checked — and sampling-based enforcement. Contract enforcement data, collected at runtime, is available for analysis. Enforcement tracing provides a mechanism for collecting data needed for experimental sampling options.
Contract clause classifications distinguish between clauses based on their type or characteristics of the contained assertions. Clause types are used for more traditional enforcement strategies; whereas assertion characteristics are intended for gathering data on the nature of contract clauses actually encountered during execution.
The SIDL specification for contract clause classification options is:
| /** * Contract classification. The classification is used to filter * contract clauses by the corresponding characteristic(s). */ enum ContractClass { /** * All classifications of interface contract clauses. */ ALLCLASSES, /** * Only constant-time complexity, or O(1), clauses. */ CONSTANT, /** * Only cubic-time complexity, or O(n^3), clauses. */ CUBIC, /** * Only invariant clauses. */ INVARIANTS, /** * Invariant plus postcondition clauses. */ INVPOST, /** * Invariant plus precondition clauses. */ INVPRE, /** * Only linear-time complexity, or O(n), clauses. */ LINEAR, /** * Method calls. Only clauses containing at least one method call. */ METHODCALLS, /** * Only postcondition clauses. */ POSTCONDS, /** * Only precondition clauses. */ PRECONDS, /** * Precondition plus postcondition clauses. */ PREPOST, /** * Only quadratic-time complexity, or O(n^2), clauses. */ QUADRATIC, /** * Only quartic-time complexity, or O(n^4), clauses. */ QUARTIC, /** * Only quintic-time complexity, or O(n^5), clauses. */ QUINTIC, /** * Results. Only clauses containing at least one assertion on an * out, inout, or result argument. */ RESULTS, /** * Only septic-time complexity, or O(n^7), clauses. */ SEPTIC, /** * Only sextic-time complexity, or O(n^6), clauses. */ SEXTIC, /** * Simple expressions. Only clauses consisting solely of * simple expressions (i.e., no method calls). */ SIMPLEEXPRS, }; |
Traditional “unit” testing with contracts at least conceptually starts with determining whether implementations comply with their specifications — assuming they are given inputs that always satisfy the stated preconditions. In this case, the POSTCONDS or INVPOST option will enable enforcement of postcondition clauses and, in the latter case, invariant clauses.
This level of testing will include determining how robust the implementations are when they are given invalid inputs. The PRECONDS or INVPRE option could be used if it is determined the implementations function properly using valid inputs. Both options enable precondition clause enforcement. The latter includes invariant clauses.
The PREPOST or ALLCLASSES option can be used if the two aforementioned phases are combined. These options will enable checking precondition and postcondition clauses. If invariants are present, the latter option, which is the default, additionally enables their enforcement.
Once implementations pass compliance testing, an integration testing phase is entered where an assessment is made of how they function in the context of the callers. At this point, if unit testing is sufficiently rigorous, the PRECONDS or INVPRE option could be used in execution time-constrained environments.
The thoroughness of the test suite is an important factor affecting the quality of the software. If the test suite is not sufficiently thorough, there is a risk of not exposing non-compliance of contract clauses in downstream methods. This situation can be of particular concern if there are dependencies involving valid sequences of method calls not exercised by the test suite.
The remaining classification options are intended for gathering data on the nature of the assertions within the contract clauses actually encountered during execution of a given program. Some options are based on the complexity of the associated assertions, inferred from the dimensions of SIDL arrays, such as CONSTANT, and LINEAR. Clearly, contract clauses involving checks of multi-dimensional arrays can be time consuming if they involve accessing many or all elements of large arrays. Another pair of options are based on the presence or absence of method calls (i. e., METHODCALLS and SIMPLEEXPRS, respectively). These options are provided since contract clauses including method calls may, depending on the work performed in the methods, be very time consuming to check. The final option is RESULTS, which is used to enable checking of clauses containing out, inout, or result arguments. It is reasoned that the data from using these options could be used for determining sources of and alternative enforcement options for high contract enforcement overhead. Such an investigation could be important in an environment where nightly regression tests cannot finish in a timely manner when checking all contract clauses encountered, for example.
Hence, contract clause classifications support traditional clause enforcement options — for checking preconditions, postconditions, and (class) invariants — as well as experimental options. The experimental options focus on the nature of assertions within contract clauses, in terms of their complexity or the presence of method calls, for example. These atypical options are intended for gathering data on the nature of contract clauses actually enforced by applications.
Enforcement frequency options range from fully and partially enabling to disabling contract enforcement. Historically, contract/assertion enforcement is fully enabled during testing and debugging but disabled during deployment. One of the reasons for disabling enforcement during deployment is that its retention has historically been considered to be too time consuming. However, there are alternatives. Some, as described in Section 21.3.1, take the form of enforcing select contract clauses. However, partial enforcement strategies based on sampling techniques can be combined with contract clause classifications to further limit enforcement.
The SIDL specification for enforcement frequency options is:
| /** * Contract clause enforcement frequency. */ enum EnforceFreq { /** * Never. Disable enforcement by completely by-passing checks * regardless of the selected contract classification. */ NEVER, /** * Always. Every clause of the selected contract classification * is enforced. */ ALWAYS, /** * Adaptive fit. Check clauses of the selected contract classification * only if they will not result in exceeding the overhead limit based * on accumulations of estimated execution times. */ ADAPTFIT, /** * Adaptive timing. Check clauses of the selected contract classification * only if their estimated execution time is within the overhead limit * applied to the estimated time of the corresponding method. */ ADAPTTIMING, /** * Periodic. Check clauses of the selected contract classification * at the specified interval. */ PERIODIC, /** * Random. Check clauses of the selected contract classifcation on a * random basis using the specified maximum. */ RANDOM, /** * Simulated Annealing. Essentially Adaptive fit but checks are * allowed to randomly exceed the overhead limit with decreasing * probability over time. */ SIMANNEAL, }; |
Basic enforcement frequency options are: ALWAYS, NEVER, PERIODIC, and RANDOM. Enabling checking all contract clauses (of the desired classification) involves using the ALWAYS option while disabling checking any contract clauses (regardless of classification) occurs when the NEVER option is used. The remaining two options represent very basic sampling strategies. PERIODIC checks clauses encountered at a specified interval while RANDOM checks a random clause (within an interval). While these two options can potentially reduce enforcement overhead, that is the extra time it takes to check the contracts, the reduction cannot be guaranteed in general, since these options do not consider the nature or (execution time) cost of the associated assertions.
WARNING:The current implementation of the experimental, performance-constrained enforcement policies has not been rigorously tested since its integration into the Babel/SIDL source code repository. Examples shown here reflect results for basic enforcement during regression testing.
The remaining options, which are experimental, are intended for use
in performance-constrained environments (e. g. nightly regression
testing of very large applications and deployment).
The options — adaptive timing (ADAPTTIMING), adaptive fit
(ADAPTFIT), and simulated annealing (SIMANNEAL) —
rely on a priori execution time estimates to conduct
performance-driven filtering of contract clauses.
Adaptive timing checks whether the execution time estimate of the
contract clause is within the user-specified overhead limit relative to the
estimate for the time required to execute the method.
Adaptive fit checks whether the execution time estimate of a clause,
added to the accumulated time of all previously checked clauses, remains
within the overhead limit of the accumulated execution time of invoked methods.
Finally, simulated annealing is essentially AdaptiveFit with
an allowance for exceeding the overhead limit, but with decreasing
probability over time.
The SIDL specification snippet for setting options associated with enforcement sampling is shown below.
| /** * <code>EnfPolicy</code> maintains the current interface * contract enforcement policy. */ class EnfPolicy { ... /** * Sets enforcement policy and options. This method should be * invoked directly to avoid the default enforcement behavior. * * @param contractClass Contract classification * [Default = ALLCLASSES] * @param enforceFreq Enforcement frequency * [Default = ALWAYS] * @param interval Sampling interval representing the * period (for PERIODIC) or maximum * random number/window (for RANDOM) * [Default = 0 if negative specified] * @param overheadLimit Limit on performance overhead [0.0 .. 1.0) * [Default = 0.0 (or 0%) if negative] * @param appAvgPerCall Average extra, application-specific * execution time, normalized by calls * to annotated methods * [Default = 0.0 if negative] * @param annealLimit Limit on simulated annealing function * to ensure its termination * (0.0 .. 2.72] * [Default = 2.72 if negative specified] * @param clearStats TRUE if enforcement statistics are to be * cleared; FALSE otherwise. */ static void setPolicy(in ContractClass contractClass, in EnforceFreq enforceFreq, in int interval, in double overheadLimit, in double appAvgPerCall, in double annealLimit, in bool clearStats); ... } |
Although the method’s documentation describes each parameter, it is worth noting that the interval is only relevant for the basic sampling techniques and the three following parameters for one or more experimental enforcement frequency option.
Execution time estimates, which are expected to be provided on a per-class basis, are assumed to be in a file conforming to the following naming convention: package-name_class-name.dat. For example, the SIDL specification below defines a package called vect with a Utils class.
| package vect { ... class Utils { /* Method signatures */ } } |
The corresponding file containing execution time estimates needs to be called vect_Utils.dat. The first line of the file is expected to contain two space-separated numbers: invariant complexity, n, and estimated average time to execute the invariants. If the are no invariants, then the first line should contain two zeros. Subsequent lines are expected to provide similar information for each method in the class, with zeros used when the clause does not apply. Specifically, lines for method estimates are expected to start with the method’s index, taken from the class’ IOR header file, followed by its precondition clause complexity, postcondition clause complexity, average execution time (without contract enforcement), average execution time of the preconditions clause, and average execution time of the postconditions clause. Supporting complexity information in the data file allows you to override the default complexity inferred from the the presence of SIDL arrays.
The file below illustrates an example estimates data file for a class that does not have an invariant clause.
| 0 0.0 12 0 1 62.34285714285714 2.7 45.857142857142854 13 0 1 44.13 3.54 166.76 6 0 0 65.04 22.8 0.0 11 0 0 301.64285714285717 4.6571428571428575 0.0 10 0 0 184.71428571428572 4.328571428571428 0.0 9 0 0 97.86666666666666 4.1 0.0 7 0 0 173.82 3.24 0.0 16 0 0 301.77777777777777 3.2666666666666666 2.566666666666667 15 0 0 214.4142857142857 2.6714285714285713 3.0714285714285716 17 0 0 174.41 3.43 2.55 18 0 0 231.01818181818183 3.2 2.481818181818182 14 0 0 177.31428571428572 2.5 4.014285714285714 8 0 0 204.10526315789474 2.4263157894736844 0.0 |
The units for the execution time estimates must be consistent across all of the estimate files association with your application program.
In summary, the enforcement frequency option is used to determine how often contract clauses are checked. Traditional enforcement is supported through ALWAYS and NEVER frequencies. Basic sampling is provided by the PERIODIC and RANDOM frequencies. Finally, three experimental sampling options — ADAPTFIT, ADAPTTIMING, and SIMANNEAL — intended for performance-constrained environments adapt enforcement based on the enforcement context, using execution time estimates.
WARNING:The current implementation of enforcement statistics gathering and reporting has not been rigorously tested since its integration into the Babel/SIDL source code repository. Examples shown here reflect results for basic enforcement during regression testing.
Data on contract enforcement is collected at runtime for
subsequent analysis.
This feature is especially important for determining relevant alternative
enforcement options for long-running regression tests and deployment.
The SIDL specification snippet for reporting enforcement statistics is given below.
| /** * <code>EnfPolicy</code> maintains the current interface * contract enforcement policy. */ class EnfPolicy { ... /** * Prints statistics data to the file with the specified name. * The file is opened (for append) and closed on each call. * * @param filename Name of the file to which the statistics * data should be written. * @param header TRUE if the header line is to be printed * prior to the statistics line (for compressed * output only). * @param prefix String description for identifying information, * if any, intended to preceed the statistics * data. Useful for distinguishing between * different objects, for example. * @param compressed TRUE if the enforcer state is to be dumped * on a single line with semi-colon separators * between fields. */ static void dumpStats(in string filename, in bool header, in string prefix, in bool compressed); ... } |
The file below illustrates snippets from the results of running the vector utilities contracts regression test available in the Babel source code distribution. The lines from the file have been reformatted to fit the width of the page.
| Prefix; Timestamp; Policy; Interval; AnnealLimit; OHLimit; procPerCall; RandSkip; CD; methTime; clauseTime; TotalRequested; TotalAllowed; Method; Checked; Okay; Violated; MethExcepts After full checking; Fri Oct 15 16:33:49 2010; Always; 0; 2.72; 0.00; 0.000; 0; 0; 20371; 524; 146; 146; vuIsZero; 5; 2; 3; 0 After full checking; Fri Oct 15 16:33:49 2010; Always; 0; 2.72; 0.00; 0.000; 0; 0; 20371; 524; 146; 146; vuIsUnit; 5; 2; 3; 0 ... After precondition checking; Fri Oct 15 16:33:49 2010; Pre; 0; 2.72; 0.00; 0.000; 0; 0; 64; 8; 5; 3; vuIsZero; 5; 2; 3; 0 After precondition checking; Fri Oct 15 16:33:49 2010; Pre; 0; 2.72; 0.00; 0.000; 0; 0; 64; 8; 5; 3; vuIsUnit; 5; 2; 3; 0 ... After Postcondition checking; Fri Oct 15 16:33:49 2010; Post; 0; 2.72; 0.00; 0.000; 0; 0; 96; 95; 6; 3; vuIsZero; 5; 2; 3; 0 After Postcondition checking; Fri Oct 15 16:33:49 2010; Post; 0; 2.72; 0.00; 0.000; 0; 0; 96; 95; 6; 3; vuIsUnit; 5; 2; 3; 0 ... After no checking; Fri Oct 15 16:33:49 2010; Never; 0; 2.72; 0.00; 0.000; 0; 0; 255; 0; 34; 0; vuIsZero; 5; 2; 3; 0 After no checking; Fri Oct 15 16:33:49 2010; Never; 0; 2.72; 0.00; 0.000; 0; 0; 255; 0; 34; 0; vuIsUnit; 5; 2; 3; 0 ... |
WARNING:The current implementation of enforcement tracing has not been rigorously tested since its integration into the Babel/SIDL source code repository.
Enforcement tracing is an advanced, experimental feature used to instrument
contract enforcement with execution timing calls.
This feature aids the collection of data for two purposes.
The primary goal is to obtain data for establishing execution time estimates
for contract clause, method, and program execution time estimates.
An alternative, which has not yet received the attention it deserves,
is to provide input for simulating the execution time overhead of
interface contract enforcement.
The SIDL specification snippet for enforcement tracing controls within the enforcement policy class is given below.
| /** * <code>EnfPolicy</code> maintains the current interface * contract enforcement policy. */ class EnfPolicy { ... /** * Starts enforcement trace file generation. * * @param filename Name of the destination trace file. * @param traceLevel Level of trace timing and reporting required. * [Default = NONE] */ static void startTrace(in string filename, in EnfTraceLevel traceLevel); /** * Returns TRUE if contract enforcement tracing is enabled; * FALSE otherwise. */ static bool areTracing(); /** * Returns the name of the trace file. If one was not provided, * the default name is returned. */ static string getTraceFilename(); /** * Returns the level of enforcement tracing. */ static EnfTraceLevel getTraceLevel(); /** * Terminates enforcement trace file generation. Takes a final * timestamp and logs the remaining trace information. */ static void endTrace(); } |
Enforcement tracing is initiated with the startTrace call and terminated with endTrace. Accessor methods — areTracing, getTraceFilename, and getTraceLevel — are provided for convenience but are not expected to be used by in general. Timing data is output to the file specified in the startTrace call as it is collected, so the traces can be very large if there are numerous calls to instrumented methods.
The SIDL specification for enforcement tracing options is:
| /** * Contract enforcement tracing levels. Enforcement traces rely on * runtime timing automatically inserted within the middleware. */ enum EnfTraceLevel { /** * None. No tracing is to be performed. */ NONE, /** * Core. Time trace start and end only. This can be useful for * simple program timing. */ CORE, /** * Basic enforcement tracing. CORE plus interface contract clause timing. */ BASIC, /** * Overhead of enforcement decisions. BASIC plus timing of * enforcement decisions. (Experimental feature.) */ OVERHEAD, }; |
So, tracing is disabled with the NONE option. The time between startTrace and endTrace calls is measured using the CORE option. Additionally, the time for checking contract clauses is obtained using the BASIC option while the enforcement decisions themselves are also timed with the OVERHEAD option.
Hence, SIDL’s experimental enforcement tracing feature facilitates gathering data for establishing the execution time estimates needed for performance-driven enforcement. The calling program is responsible for starting and stopping tracing through the methods provided in SIDL’s enforcement policy class. Tracing data is currently output as it is collected, resulting in additional file I/O overhead during execution.
This chapter describes extensions to the Babel toolkit for the specification and enforcement of interface contracts. SIDL allows the specification of executable, Eiffel-inspired precondition, postcondition, and class invariant clauses. Each clause may contain one or more assertion expressions using traditional and advanced operators as well as built-in and user-defined functions. The SIDL Runtime currently supports global interface contract enforcement, on a clause basis, through a range of enforcement options combining contract clause classification and enforcement frequency options. Optional enforcement tracing, which can be used to collect relevant execution time data, is also supported. Detected violations result in clause-specific exceptions identifying the violated assertion.
WARNING:Not all capabilities described in this chapter have been tested. In particular, regression tests exercising class invariants and a number of the built-in functions available for use in contract clauses are still pending. In addition, built-in functions are currently limited to one- and two-dimensional arrays. Furthermore, the experimental enforcement policies and enforcement tracing need to be re-tested after their integration into the Babel/SIDL repository.