Static Contract Simplification
Matthias Keil, Peter Thiemann
TL;DR
This paper introduces a static program transformation technique to simplify contracts in code, reducing runtime overhead of contract checks while maintaining behavior, through contract propagation and merging.
Contribution
It proposes a novel static transformation method that reduces runtime contract checking overhead by propagating and merging contracts at compile time, preserving program behavior.
Findings
Transformations never increase contract checks
Effective contract propagation and merging reduces runtime overhead
Supports different levels of blame preservation
Abstract
Contracts and contract monitoring are a powerful mechanism for specifying properties and guaranteeing them at run time. However, run time monitoring of contracts imposes a significant overhead. The execution time is impacted by the insertion of contract checks as well as by the introduction of proxy objects that perform delayed contract checks on demand. Static contract simplification attacks this issue using program transformation. It applies compile-time transformations to programs with contracts to reduce the overall run time while preserving the original behavior. Our key technique is to statically propagate contracts through the program and to evaluate and merge contracts where possible. The goal is to obtain residual contracts that are collectively cheaper to check at run time. We distinguish different levels of preservation of behavior, which impose different limitations on the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Logic, programming, and type systems · Advanced Malware Detection Techniques
\copyrightdata
978-1-nnnn-nnnn-n/yy/mm \copyrightdoinnnnnnn.nnnnnnn
\preprintfooter
Static Contract Simplification
\authorinfo
Matthias Keil and Peter Thiemann University of Freiburg,
Freiburg, Germany {keilr,thiemann}@informatik.uni-freiburg.de
Static Contract Simplification
Technical Report
(20yy)
Abstract
Contracts and contract monitoring are a powerful mechanism for specifying properties and guaranteeing them at run time. However, run time monitoring of contracts imposes a significant overhead. The execution time is impacted by the insertion of contract checks as well as by the introduction of proxy objects that perform delayed contract checks on demand.
Static contract simplification attacks this issue using program transformation. It applies compile-time transformations to programs with contracts to reduce the overall run time while preserving the original behavior. Our key technique is to statically propagate contracts through the program and to evaluate and merge contracts where possible. The goal is to obtain residual contracts that are collectively cheaper to check at run time.
We distinguish different levels of preservation of behavior, which impose different limitations on the admissible transformations: Strong blame preservation, where the transformation is a behavioral equivalence, and weak blame preservation, where the transformed program is equivalent up to the particular violation reported. Our transformations never increase the overall number of contract checks.
category:
D.3.1 Formal Definitions and Theory Semantics
category:
D.2.4 Software/Program Verification Programming by contract
††conference: CONF ’yy Month d–d, 20yy, City, ST, Country
1 Introduction
Software contracts Meyer [1988] stipulate invariants for objects as well as pre- and postconditions for functions a programmer regards as essential for the correct execution of a program. Traditionally, contracts are checked at run time by contract monitoring. This approach has become a prominent mechanism to provide strong guarantees for programs in dynamically typed languages while preserving their flexibility and expressiveness.
Using formal and precise specifications in the form of contracts in this way sounds appealing, but it comes with a cost: Contract monitoring degrades the execution time significantly Takikawa et al. [2016]. This cost arises because every contract extends a program with additional code to check the contract assertions that needs to be executed on top of the program. Moreover, human developers may inadvertently add contracts to frequently used functions and objects so that contracts end up on hot paths in a program. In particular, if contracts are naively applied to recursive functions, predicates will check the same values repeatedly, which aggravates the performance degradation.
Existing contract systems for dynamically typed languages (e.g., Racket’s contract framework [Flatt et al., 2014, Chapter 7], Disney’s JavaScript contract system contracts.js Disney [2013], or TreatJS for JavaScript Keil and Thiemann [2015b]) each suffer from a considerable performance impact when extending a program with contracts.
In contrast, static contract checking Xu et al. [2009] avoids any run-time cost if it succeeds in proving and removing a contract at compile time. Otherwise, it defers to plain contract checking. A subsequent extension to hybrid contract checking Xu [2012] is able to exploit partial proofs and to extract a residual contract that still needs to be checked at run time. Both of these works are phrased as transformations in a typed intermediate language.
A similar motivation is behind static contract verification Nguyen et al. [2014]. This work takes place in the context of an untyped language. It applies symbolic execution as well as techniques from occurrence typing to prove contracts statically and thus eliminate their run-time overhead.
Our work is complementary to these previous efforts. Our main objective is to improve the efficiency of contract monitoring by using static techniques to evaluate as much of a contract as possible, to detect and remove redundant checking of contracts, and to reassemble the fragments that cannot be discharged statically in places where they are least likely to affect performance. Typically, we move contract fragments to a surrounding module boundary and compose them to a new contract.
Thus, our goal is not to detect contract violations at compile time, but rather to optimize contracts based on static information. We also do not rewrite the non-contract code of the underlying program, but perform program transformations restricted to just moving around contracts.
To demonstrate the essence of our approach, consider the following code snippet that contains a function with an intersection contract applied to it.
The value addOne is a function that takes an argument z and returns the result of applying function plus to the number 1 and to z. We use the inline operator @ to indicate contract assertions that we put in square brackets to improve readability. We further rely on predefined flat contracts Number*?* and String*?* that are type checks for numbers and strings, respectively.
If we assume that the + operator is overloaded as in JavaScript or Java so that it works for number and string values (but possibly fails or delivers meaningless results for other inputs), a programmer may add an intersection contract to plus. This contract has the effect that the context of a use of plus (here function addOne) can choose to use plus either with number or string arguments. Monitoring this contract requires six predicate checks at every use of addOne.111Assuming the semantics of intersection and union contracts from the literature Keil and Thiemann [2015a].
However, as the second argument of plus is already a number, the right side of the intersection can never be fulfilled. So, it would be sufficient to check if the first argument of plus and its return value satisfy Number*?*. Moreover, the remaining predicates can be lifted to an interface description on addOne, as the following example demonstrates. Only two predicate checks remain.
This simplification can be done without knowing whether addOne is ever executed: we are not losing any blame due to the transformation. However, it would not be ok to lift argument contracts across function boundaries. Such lifting would introduce checks that may never happen in the original program.
Building on the formalization of Keil and Thiemann [2015a], we present a transformation system for static contract simplification. Our system provides two stages of simplification with different consequences: The Baseline Optimization and the Subset Optimization.
The Baseline Optimization unfolds contracts and evaluates predicates where possible while preserving the blame behavior of a program. The Subset Optimization reorganizes contracts and forms new contracts from the contract fragments, but it may reorder contract computations and thus change the blame (i.e., the particular violation that is flagged at run time). Our simplification rules respect three overall guidelines:
Improvement
Each transformation step improves the efficiency of contract monitoring: it either reduces or maintains the total number of predicate checks at run time. Simplification never increases the number of run-time checks.
Strong Blame-Preservation
Each transformation step of the baseline simplification fully preserves the blame-behavior of a program. It maintains the oder of contract checks at run time and thus the order in which violations are reported. A transformed program produces the same outcome as the original program.
Weak Blame-Preservation
Transformation steps of the subset simplification may change the oder of predicate checks, so that they may also change the order of observed violations. Thus, a transformed program ends in a blame state if and only if the original program would end in a blame state. However, the transformed program may report a different violation.
An optional third level optimizes contracts across module boundaries. Even though it provides the strongest optimization, it may over-approximate contract violations and it would violate all three guideline from above.
Contributions
This work makes the following contributions:
- •
We present the semantics of a two-tier static contract simplification that reorganizes and pre-evaluates contracts at compile time while guaranteeing weak or strong blame preservation.
- •
We show how to split alternatives into separated observation to deal with intersection and union contracts.
- •
We give a specification of subcontracting that is used to simplify contracts based on the knowledge of other asserted contracts.
We created an executable implementation of the semantics using PLT Redex Felleisen et al. [2009]. The implementation is available online at http://anonymous.
Overview
Section 2 provides a series of examples demonstrating the essence of our contract simplification. Section 3 recalls contracts and contract satisfaction from the literature and introduces an untyped, applied, call-by-value lambda calculus with contract monitoring. Section 4 introduces Baseline Simplification, the first tier in our simplification stack. Section 5 shows the second tier, Subset Simplification, which also handles alternatives and reduces contracts that are subsumed by other contracts. Section 6 states our blame theorems and Section 7 briefly addresses run time improvements. Section 8 discusses related work and Section 9 concludes.
The appendix extends this paper with auxiliary functions and definitions, further examples, and proofs of all theorems. In particular, it provides the semantics to enable picky-like evaluation semantics and the semantics of a third, approximating, simplification level that provides the stringes simplification.
2 Contract Simplification
This section explains the main ideas of our transformation through a series of examples. We start with a simple example and work up to more complex ones.
2.1 Unrolling Delayed Contracts
The examples consider different contracts on the addOne example from the previous section. In a first step we add a simple function contract to plus.
While Number*?* is a flat contract that is checked immediately, function contracts are delayed contracts. A delayed contract cannot be checked directly when asserted to a value. Delayed contracts stay attached to a value and are checked when the value is used. Thus, every call to addOne triggers three predicate checks.
Instead of asserting a contract that forces a number of delayed contract checks, our Baseline Simplification unrolls a delayed contract to all uses of that value. This step pushes the delayed contract inwards to all occurrences of plus in addOne.
This step performs no simplification, but it yields an equivalent program that is better prepared for unfolding the function contract to its domain and range because the contract is on an expression in application position. The following snippet demonstrates the (complete) unfolding of the contract, which combines a number of primitive unfolding steps.
In the resulting expression, the function contracts are completely decomposed into flat contract components which are spread all over the expression.
Observe that, after unfolding, there are several flat contracts applied to values. Such contracts can be checked statically without changing the outcome. For example, 1 satisfies Number*?*. All satisfied contracts can safely be removed from the program.
In a last step, we push the remaining contract fragments outwards where possible. This transformation creates a new function contract from that contract. The special contract accepts every value.
Afterwards, the outermost expression carries a function contract that checks the return value of addOne and one contract is left in the body of addOne to check the argument. Again, this step does not simplify contracts, but it prepares for further simplification steps.
However, further simplification cannot be done while guaranteeing strong blame preservation. The Baseline Simplification is not allowed to behave differently than the dynamics would do at run time.
2.2 Treating Intersection and Union
Our next example considers the full addOne example from the introduction, which we repeat for convenience.
Intersections of function contracts are delayed contracts, they must stay attached to a value until the value is used in an application. Moreover, for an intersection, the context can choose to fulfill the left or the right side of the intersection. Thus, every call to addOne triggers six predicate checks.
Again, Baseline Simplification unrolls the intersection contract to all uses of that value and unfolds the contract to its domain and range when used in an application. The following snippet demonstrates the unfolding of the intersection contract.
In addition, the static contract monitor maintains additional information in the background (e.g., which contracts belong to the same side of the intersection) to connect each contract with the enclosing operation. In the example we indicate the originating operand of the intersection by @ and @.
After unfolding, the Baseline Simplification checks flat contracts applied to values. Here, 1 satisfies Number*?* but violates String*?. While Number?* can now be removed, information about a failing contract must remain in the source program. In general, it is not possible to report failure statically because we do not know if the code containing the failed contract (in this case, function addOne) is ever executed.
However, we do not have to leave the original contract in the expression. Instead, the transformation replaces it by a “false contract” , whose sole duty is to remember a contract violation and report it at run time. The next snippet shows the result after processing satisfied and failing contracts and pushing the remaining fragments outwards.
Afterwards, the outermost expression carries two function contracts that check the return value of addOne; two contracts are left in the body of addOne to check the argument.
2.3 Splitting Alternatives in Separated Observations
When remembering the last state in Section 2.2, we still check String*?* even though we know that right side of the intersection is never fulfilled. This is because the Baseline Simplification preserves the blame behaviour of a program and is thus not able to deal with alternatives. However, the next Subset Simplification abandons the strong blame preservation to further optimize contracts.
Instead of unfolding intersection and union contracts, we now observe both alternatives in separation. After transforming both alternatives, we join the remaining contracts or even discard a whole branch if it definitely leads to a violation.
In our example, we see that 1 @ String? leads to a context failure of the right operand of the intersection contract. Thus, it is useless to keep the other fragments of the right operand which definitely yields a context violation. The following code snippet shows the result.
It remains to check z and addOne’s return to be a number. This are two remaining checks per use of addOne.
However, we still need to keep the information on the failing alternative. This is required to throw an exception if also the other alternative fails.
2.4 Lifting Contracts
As shown in the example above, contracts on the function’s body are reassembled to a new function contract, whereas contracts on function arguments must remain to preserve the order of predicate checks. Continuing the example, our next step constructs a new contract from the remaining contracts on arguments.
The addOne function now contains another function contract that restricts its domain to number values. As this step puts contracts on arguments in front, it may change the order in which violations arise. This lifting to module boundaries only reorganizes existing contracts, but it helps to reduce contracts that are subsumed by other contracts.
2.5 Condensing Contracts
Continuing the example in Section 2.4, the outermost expression carries two function contracts that check the argument and the return value of addOne. Moreover, both contracts arise from the same source contract. These function contracts may be condensed to a single function contract on addOne.
This step is only possible if the argument contract, here Number*? , is in negative position and if the return contract, Number?* is in positive position.
2.6 Contract Subsets
Splitting intersections and unions into separate observations has another important advantage: We know that in every branch every contract must be fulfilled. Thus we can relate contracts to other contracts and use knowledge about other contracts to reduce redundant checks. To demonstrate an example, we add a second contract to our running example.
Here, Positive*?* is a flat contract that checks for positive numbers. In addition to the contract on plus, addOne contains another function contract, requiring addOne to be called with positive numbers and to return a positive number. After performing the same transformation steps as before, we obtain the following expressions.
The intersection is split into two parallel observations, as indicated by . All contracts were pushed to the outermost boundary and form a new module boundary. However, some of the contract checks are redundant.
For example, the innermost contract in the first observation requires addOne to be called with numbers, whereas the outermost contract restricts the argument already to positive numbers. As positive numbers are a proper subset of numbers, the inner contract will never raise a violation if the outer contract is satisfied. Thus, it can be removed without changing the blame behavior of a program.
The contract Positive*? Positive?* is more restrictive than any other contract on addOne, that is, Number*? * and * Number?*. Here, a contract is more restrictive than a contract , if the satisfaction of implies the satisfaction of .
However, if a more restrictive contract fails, that failure does not imply failure of the less restrictive contract. But as every contract must be fulfilled, the program already stops with a contract violation. Thus, there is no need to check a less restrictive contract on that branch. Unfortunately, removing the less restrictive contract might change the order of observed violations, as the less restrictive contract might report its violation first.
To sum up, in the first observation the outer contract remains as it subsumes any other contract, whereas in the second observation both contracts remain.
Finally, after finishing all transformation steps, the simplifications joins the observation to final expression.
3 Contracts and Contract Satisfaction
This section defines , an untyped call-by-value lambda calculus with contracts which serves as a core calculus for contract monitoring. It first introduces the base calculus , then it proceeds to describe contracts and their semantics for the base calculus. Finally it gives the semantics of contract assertion and blame propagation.
The core calculus is inspired by previous work from the literature Keil and Thiemann [2015a].
3.1 The Base Language
Figure 1 defines syntax and semantics of , an applied call-by-value lambda calculus. A term is either a first-order constant, a variable, a lambda abstraction, an application, a primitive operation, or a condition. Variables , , and are drawn from a denumerable set of variables. Constants range over a set of base type values including booleans, numbers, and strings.
To define evaluation, values , , and range over values and over evaluation contexts, which are defined as usual.
The small-step reduction relation comprises beta-value reduction, built-in partial operations transforming a vector of values into a value, and the reduction of conditionals. We write for its reflexive, transitive closure and for its complement. That is, if, for all such that , it holds that . We also write to indicate that there is no such that .
3.2 Contracts and Contracted
Figure 2 defines the syntax of as an extension of . It first introduces constructs for contract monitoring in general and, second, it adds new terms specific to contract monitoring. Intermediate terms that do not occur in source programs appear after double bars “”.
A contract is either an immediate contact , a delayed contract , a union between two contract , or an intersection .
Without loss of generality we restrict top-level intersection contracts to intersections between an immediate contract and a rest contract (cf. Keil and Thiemann [2015a]). This requires that unions and immediate parts are distributivity pulled out of intersections of delayed contracts such that the immediate parts can be check right away when asserted, whereas the delayed parts remain.
Immediate contracts and stand for flat contracts define by a predicate that can be evaluated right away when asserted to a value.
A delayed contracts is either a function contract with domain contract and range contract , a dependent contract defined by contract abstraction , or the finite intersection of function (dependent) contracts. Delayed contracts stay with the value until the value is subject of an application.
Consequently, values are extended with which represents a value wrapped in a delayed contract that is to be monitored when the value is used. The extended set of values forces us to revisit the built-in operations. We posit that each partial function first erases all contract monitoring from its arguments, then processes the underlying -values, and finally returns a -value.
The only new source term is contract assertion . The adornments and are drawn from an unspecified denumerable set of blame identifiers , which comprises blame labels that occur in source terms and blame variables that are introduced during evaluation.
In the intermediate term , the term represents the current evaluation state of the predicate of a flat contract. The expression signal a contract violation at label . Term B is either a +blame (positive) or a -blame (negative) blame, representing subject or context blame, respectively.
Evaluation contexts are extended in the obvious way: a contract monitor is only applied to a value and a flat contract is checked before its value is used.
In , contract monitoring occurs via constraints imposed on blame identifiers. There is an indirection constraint and one kind of constraint for each kind of contract: flat, function, intersection, and union. Constraints are collected in a list during reduction.
3.3 Semantics for
Figure 3 specifies the small-step reduction semantics of as a relation on pairs of a constraint list and a term. Instead of raising blame exceptions, the rewriting rules for contract enforcement generate constraints in : a failing contract must not raise blame immediately, because it may be nested in an intersection or a union. The sequence of elements in the constraint list reflects the temporal order in which the constraints were generated during reduction. The latest, youngest constraints are always on top of the list. Appendix A explains the semantics of the constraints.
The rule Assert introduces a fresh name for each new instantiation of a monitor in the source program. It is needed for technical reasons. Flat contracts get evaluated immediately. Rule Flat starts evaluating a flat contract by evaluating the predicate applied to the unwrapped subject value . Meta function (Figure 4) first erases all contract monitors from the subject value . After predicate evaluation, rule Unit picks up the result and stores it in a constraint.
The second group of rules Union and Intersection implements contract checking of top-level union and intersection contracts. Both rules install a new constraint that combine the contract satisfaction of the subcontracts to the satisfaction of the current contract.
The rules D-Function, D-Dependent, and D-Intersection define the behavior of a contracted value under function application. Rule D-Function handles a call to a value with a function contract. Different from previous work, the blame computation is handled indirectly by creating new blame variables for the domain and range part; a new constraint is added that transforms the outcome of both portions according to the specification of the function contract.
The D-Dependent rule defines the evaluation of a dependent contract. It substitutes the function’s arguments for every occurrence of in the body of and proceeds with the assertion of the resulting contract.
Rule D-Intersection embodies the evaluation of an intersection contract under function application. The generated constraint serves to combine the results of the subcontracts. Unlike the union contract, an intersection constraint occurs at each use of the contracted value, which implements the choice of the context (cf. Keil and Thiemann [2015a]).
Finally, reductions are lifted to reductions using rule Base. Built-in operations and conditions “see through” contracts (rules D-Op and D-If) and proceed on -values without contracts. This also implies that all base type operations only return values that does not contain contracts.
3.4 Introducing Blame
The dynamics in Figure 3 use constraints to create a structure for computing positive and negative blame according to the semantics of subject and context satisfaction, respectively. To this end, each blame identifier is associated with two truth values, and . Intuitively, if is false, then the contract associated with is not subject-satisfied and may lead to positive blame for . If is false, then there is a context that does not respect contract and may lead to negative blame for . Appendix A specifies the constraint satisfaction for .
Computing a blame assignment boils down to computing an interpretation for a constraint list . To determine whether a constraint list is a blame state (i.e., whether it should signal a contract violation), we check whether the state maps any source-level blame label to false.
Definition 1**.**
* is a blame state for blame label iff*
[TABLE]
* is a blame state if there exists a blame label such that is a blame state for this label.*
To model reduction with blame, we define a new reduction relation on configurations. It behaves like unless is a blame state. In a blame state, it stops signaling the violation. There are no reductions with B.
[TABLE]
3.5 Lax, Picky, and Indy Semantics
Contract monitoring distinguishes three blame semantics: Lax, Picky, and Indy, initially introduced to handle correctness and completeness of higher-order dependent contracts Dimoulas et al. [2011]. The different styles address the point that a contract might violate another contract.
The Lax semantics erase all contract monitors on values before applying a value to a predicate. This is correct but not complete because it guarantees that a well-behaved program gets never blamed for a violation taking place in a predicate. However, it omits to report violations in predicates.
The Picky semantics, in contrast, is complete but not correct. As it retains contract monitors on the values it might wrongly blame the program for violating a contract, but it guarantees that every violation is reported.
The Indy semantics, an extension of Picky, introduces a third party (the contract itself) in addition to the exiting parties context and subject. Passing a value to a predicate reorganizes the monitor such that wrong uses of that value blame the ill-behaved contract.
Our optimization considers the Lax style, as it strongly guarantees correctness and completeness in respect to source program. As reorganizing contracts changes the order of predicate checks optimizing is simpler when using Lax semantics.
Appendix D discusses our simplification with respect to Picky like evaluation semantics.
4 Baseline Simplification
This section presents the Baseline Simplification, the first tier in our simplification stack. The baseline simplification encompass
(i) the unfolding of contract assertions and the creation of constraints where possible,
(ii) the compile-time evaluation of flat contracts (predicates) on values, and
(iii) the unrolling of delayed contracts to all uses of the contracted values.
To this end, we introduce a set of canonical (non-transformable) terms as a subset of terms and extend syntax and semantics of in some respects.
All baseline steps do exactly the same as the dynamics would later on do. Thus, baseline simplification guarantees Strong Blame-preservation and Improvement for all transformation steps.
4.1 Syntax and Semantics Extension
Figure 5 shows some syntax extension for .
Contracts now contain (true) and (false), shortcuts for predicates evaluating to true or false, respectively. and arise during optimization and represent remaining knowledge about the given proposition. Whereas can be reduced statically, must remain in the source program to ensure correct blame propagation.
The shortcuts are more efficient because none of them must be checked at run time. When reaching a term with or the outcome can immediately be transfered into a constraint and must not be checked like a predicate.
Source terms now contain partially evaluated contracts on source terms and a new inversion constraint extends the set of constrains . The inversion constraint flips context and subject responsibility and corresponds to the negative side of a function constraint. This constraint only arises during optimization.
Figure 6 specified the reduction of the shortcuts. Rule Reduce/True and Reduce/False creates a constraint for and . Three special rules, D-Domain, D-Range, and D-False simplify the evaluation of function contracts with and on its domain or range portion. If one portion is true only the other portion must be checked. All this function contrast arise only during optimization.
4.2 Canonical Terms and Contexts
Canonical (non-transformable) terms are the output of our transformation. A canonical terms is either a contract-free term or a term with a contract that cannot further transformed at this level.
In general, canonical terms distinguish terms without a contract on the outermost level (indicated by letter ) from terms with a non-transformable contract (indicated by letter ). Canonical terms are a subset of terms . Appendix B.1 shows its definition.
A transformation context , , and (Figure 7) is defined as usual as a term with a hole and a value context is a term with an indefinite number of remaining contracts. This terms result only during transformation.
4.3 Baseline Transformation
The baseline transformation is defined on pairs of a constrains list and terms. As before, we write for its reflexive, transitive closure.
Figure 8 specifies the baseline transformation rules for terms . The first rules, Unfold/Assert, Unfold/Union, and Unfold/Intersection, unfold contracts and create constraints equivalent to the dynamics in Subsection 3.5.
Rule Unfold/Op unpacks a delayed contract on a term used in a base type operation. As this contract is never checked, it is true by definition (cf. Keil and Thiemann [2015a]). Here, terms and are canonical terms with a possible immediate or delayed contract.
Rules Unfold/D-Function and Unfold/D-Intersection unfold a delayed contract that appears left in an application corresponding to the dynamics. However, a function contract unfolds the domain portion to the term on the right, which is not necessarily a value.
Rule Unroll unrolls a delayed contract on a term right in an application. This step removes the contract from and grafts it to all uses of . Even though this steps duplicates the number of contract assertions, we do not have more contract checks.
Rule Lower create a new function contract by lowering the contract on the function’s body. The new function contract contains on it’s domain portion as it accepts every argument.
Rules Push/Immediate and Push/False reverse the order of a delayed contract nested in an assertion with an immediate contract or . This step is required to evaluate immediate contracts on values and to unfold or unroll function’s contracts.
Rule Push/If pushes a contract out of a condition if the contracts appears on both branches of the condition.
Rule Convert/True reduces all occurrences of and produces a constraint that maps true to the corresponding blame variable . Knowledge about satisfied contracts can safely be removed from the source program because they do not compromise the blame assignment.222Due to the specification of contract satisfaction it is also possible to remove from the source program without creating a constraint. A non-existing constraint is handled as true because every non-violated contract assertion is satisfied, either because it is fulfilled or never verified.
In contrast to , (the knowledge about a failing contract) must remain in the source program and cannot be translated into a constraint statically. Doing this would over-approximate contract failures as the constrain might lead to a blame state, without knowing if the ill-behaved sources is ever executed. However, over-approximating violations might be intended, as Appendix G demonstrates.
Finally, rules Verify/True and Verify/True evaluate flat contracts on values that are available at compile time and transform the outcome of the evaluation into or . Values might be nested in a number of contracts of previously checked predicates.
Lemma 1** (Progress).**
For all terms it holds that either is a canonical term or there exists a transformation step .
4.4 Strong Blame-preservation
To sum up, the Baseline Transformation makes exactly the same transformation steps at compile time, than the dynamics would later on do. Thus, preserves the evaluation behavior of our program.
Conjecture 1** (Strong Blame-preservation).**
For all transformations it hold that either and or that and .
5 Subset Simplification
The Subset Simplification is the second tier in our transformation stack. Its objective is to reuse knowledge of previously checked contracts to avoid redundant checks whenever possible and to propagate contract violations to the surrounding module boundary.
The transformation first branches every alternative given by intersection and union contracts into an individual observation on which every contract must be fulfilled. Later it reduces contracts that are less restrictive and subsumed by other contracts. Finally, it joins remaining fragments to a new contract where possible.
To this end we introduce a subcontract relation which is closely related do already existing definitions of naive subtyping. Subcontracting claims a contract to be more restrictive than another contract.
5.1 Predicates
To achieve the best possible result it requires to have contracts and predicates as fine grained as possible. Intersection and union contracts enable to build complex contracts from different sub-contracts. Distinct properties can be written in distinct predicates (flat contracts) and combined using intersection and union.
For example, a contract that checks for positive even numbers can be written as the intersection of one contract that checks for positive numbers and one contract that checks for even numbers:
[TABLE]
However, there is a twist. Fine-grained sub-contracts enable contracts be optimized efficiently. But, at evaluation time, they must be handled in separation such that we result in more predicate checks.
For example, consider the following contract that checks for natural numbers:
[TABLE]
Obviously, one can write a similar contract like this:
[TABLE]
The presence of intersection and union contracts enables developers to write fine grained contracts, which, in turn, enable us to identify redundant parts and to reduce already checked properties.
To avoid a run time impact cause by fine-grained predicates, we can easily conjunct or disjunct predicates of the same blame label after optimization. This is possible because the intersection and union of flat contracts corresponds to the conjunction and disjunction of predicates (cf. Keil and Thiemann [2015a]).
5.2 Contract Subsets
When optimizing contracts, we use subcontracting to characterize when a contract is more restrictive than another contract, i.e. it subsumes all of its obligations. The definition of subcontracting is closely related to naive subtyping from the literature Wadler and Findler [2009].
We write if is more restrictive than , i.e. implies that and implies that .
As a contract specifies the interface between a subject and its enclosing context, subcontracting must be covariant for both parties: context and subject.
For example, let Positive*? = flat(,\x.x>0)* and Natural*? = flat(,\x.x0). Than Positive?* Natural*?* as for all x it holds that x*>0* implies x**0.
For another example, Positive*? Positive?* is a subcontract of Natural*? Natural?* as it is more restrictive on both portions. Furthermore, Positive*? Natural?* and Natural*? Positive?* are further subcontracts of Positive*? Positive?*.
In order to specify our subcontracting judgement, we factor subcontracting into two subsidiary relations: subject subcontracting, written , and context subcontracting, written . Relation indicates that the subject portion in is more restrictive than the subject portion in , whereas indicates that restricts the context more than .
In contrast to Wadler and Findler’s definition of positive and negative subtyping (cf. Wadler and Findler [2009]), which is related to ordinary subtyping, our definition of positive and negative subcontracting is reversal because its is related to the naive subcontracting. We write if is more restrictive than , whereas Wadler and Findler write .
Figure 9 shows both relations. The two judgement are defined in terms of each other and track swapping of responsibilities on function arguments. Both judgements are reflexive and transitive.
We further write if predicate implies predicate . For example, (x>0) (x0) and (x=0) (x0).
However, our subcontract judgement stops at . Relation refers to an environment that resolves relations on terms. might be given by a SAT solver or a set of predefined relations.
[TABLE]
It remains to defined subcontracting in terms of context and subject subcontracting.
Definition 2**.**
* is a naive subcontract of , written , iff*
[TABLE]
We further define an ordinary subcontracting judgement, , which corresponds to the usuals definition of subtyping. Ordinary subcontracting is contravariant for the context portion and covariant for the subject portion.
Definition 3**.**
* is an ordinary subcontract of , written , iff*
[TABLE]
In addition to the already mentiont notation, we sometimes use , , , and to indicate a proper subcontract, analogous to already existing definitions on inequality.
Lemma 2**.**
Relation is a preorder, i.e. it is reflexive and transitive. For all , , and , we have that:
- •
**
- •
if and then
5.3 Canonical Terms, revisited
As for the Baseline Transformation, we first define a set of canonical terms (non-transformable) terms that serve as the output of this level’s transformation. The new canonical terms are a subset of the already defined terms in Section 4.2. Appendix B.2 shows its definition.
In addition, Figure 10 shows the definition of a new transformation contexts that looks through parallel observation. An assertion context is a number of contract assertions and a body context is a transformation context without lambda abstractions and without conditions with a hole in a branch.
5.4 Subset Transformation
Figure 11 defines the subset transformation as an extension of the baseline transformation in Figure 8.
A significant change is that the new rules Fork/Union and Fork/Intersection replace the already exiting rules with the name Unfold/Union and Unfold/D-Intersection. Both rules split the current observation and handle both sides of an intersection or union in separation. This step eliminates alternatives such that in each branch every contract must be fulfilled.
Doing this enables us to remove a contracts whose properties are subsumed by another contracts. Without splitting alternatives it would not be possible to remove a contract on the basis of other contracts: The other contracts might be nested in an alternative and thus it might never apply (as there is a weaker alternative).
As for the baseline rules, unions are split immediately when asserted to a value, whereas intersections must remain on the values until the values is used in an application. This is because the context can choose between both alternative on every use of the value.
Rule Unfold/Intersection (Figure 8) must not be redefined, as the intersections with flat contracts is equivalent to a conjunction of its constituents (cf. Keil and Thiemann [2015a]).
Rule Lift lifts an immediate contract on a variable bound in a lambda abstraction and produces a function contract on that abstraction. However, at this level we are only allowed to lift contracts on variables directly contained in the function body. Lifting from a deeper abstraction would introduce checks that might never happen at run time.
Second, it is only allowed to lift an immediate contract. This is because a lifted delayed contract would remain on the argument value and thus it would effect all uses of that value, which entirely changes the meaning of the program.
Rule Lower pushes a contract on a function body down and creates a new function contract from that contract. But now we have the restriction that the function’s return is not it’s argument.
Rule Blame transforms a function body to a blame term in case a contract violation happens in that body. As we split alternatives we know that every contract must be fulfilled, and thus violating a contract immediately results in a contract violation for that branch. However, we cannot transform the whole execution to as we do not know if the body es ever executed (e.g. because its is nested in a condition or the lambda term is never used in an application).
Here, computes a blame term resulting from a predicate violation () in (cf. Appendix C.3).
As before, must remain on the term to remember the violated contract. However, as the whole body transforms to , may stay as a contract on a function body. In this case, rule Lower pushes the information of a failing contract down to the enclosing body, which in turn is unrolled when used in an application and rule Blame transforms the enclosing context to . Appendix H shows an example reduction.
The rules Blame/If/True and Blame/If/False do the same if a blame appears in branch of a conditions and rule Blame/Global produces a global blame term if appears on a top-level term.
Rules Subset/Left and Subset/Right removes a contract from a term that is less restrictive than another contract on that term. As this step removes a contract it might change the order of arising contract violations. The weaker contract might raise a contract violation before the stronger contract is checked. But, as the stronger contract remains, we know that we definitely result in a blame state until the stronger contract is satisfier. And, by definition, this implies that the weaker contract is also satisfied.
Rule Push/If pushes a contract out of an condition if the contract remains ob both branches of the condition.
Rule Merge merges remaining fragments of the same source contract to a new function. However, this can only be done if both contracts have the same responsibility, which is indicated by precondition .
Finally, the rule Baseline lifts baseline transformations to subset transformations, and rule Trace considers the transformation in a parallel observation.
Lemma 3** (Progress).**
For all terms it holds that either is a canonical term or there exists a transformation step .
Apart from the subset transformation which uses native subcontracting to reduces contracts subsumed by other contract, we also use ordinary subcontracting to simplifiy contracts contained in an intersection or union contract. Appendix F demonstrates this.
5.5 Join Traces
The subset transformation splits intersection and union into separated observation, i.e. its outcome is a set of parallel observations. Thus, after transforming all observations to canonical terms, we need to join the remaining fragments to a valid source program.
Joining terms must be one of the last step as it is not possible to apply further transformations afterwards. Subsequent transformations would mix up contracts from different alternatives and thus they may change the meaning of a contract.
To this end, Figure 12 defines a context , which is defined as usual as a term with a hole. The only exception is that contexts did not have holes in a contract assertion.
As our transformation did not change the basic syntax of a program (it only propagates contracts), terms remain equivalent (excepting contract assertions) until they transform to a blame term. It follows that the only difference between parallel terms are contract assertions and blame terms.
We call terms that differ only in contract assertions and blame terms as structurally equivalent. We write if term is structurally equivalent to term and for the structural equivalence of contexts.
Definition 4**.**
Two terms are structural equal, written , if they only differ in contract assertions and blame terms.
Definition 5**.**
Two contexts are structural equal, written , if they only differ in contract assertions and blame terms.
Figure 13 shows the structural equivalence of terms and contexts. The equivalence relations looks through contract assertions and compares only terms.
Lemma 4**.**
Relation on terms and context is an equivalence relation.
To join terms in parallel observations we only need to walk through all terms and to synchronise contract assertions and blame terms. Figure 14 presents the synchronisation of contracts and terms, indicated by relation on terms.
First, rule Join triggers the synchronization of two canonical terms nested in a parallel observation and rule Match dissolves a parallel observation if both terms are identical.
The rules Synchronize/Left and Synchronize/Right handle the case that one side results in a blame state. In this case the blame term is omitted and the operation proceeds with other term. Remember, it is not required to maintain the blame term because still remains in the source program.
Finally, rule Synchronize/Contract looks for different contract assertions on a term and merges the contract assertions. Precondition requires that the enclosing contexts are structurally equivalent. Only the contract assertions must be different.
Here, computes the union of both contexts and synchronizing proceeds with the new context in place.
The easiest way to merge contexts is to place one context in the hole of the other context. Even through this did not change the blame behaviour of a program it might duplicate contract checks, and thus it violates our ground rule not to introduce more checks.
Thus, merging assertion contexts only places contract assertions in the hole that are not already contained in the context. Formally, we specify the join of two assertion contexts and by
[TABLE]
Here, computes a new context with assertions from that are not already contained in . Appendix C.4 shows its computation.
5.6 Condense Remaining Contracts
Finally, one last step remains to be done: After synchronizing contracts it might happen that we have identical contracts on the same term. As they belong to different alternatives we cannot remove one of them, but we can condense them a single assertion.
Figure 15 shows the transformation. If a term has two assertions of the same contract, Rule Condense removes one of them and creates a new constraint that redirect the result from the other assertion to the blame variable of the remove assertion.
5.7 Bringing all this together
To model transformation with parallel observations, we define a new transformation on terms . It first applies the standard transformation until it reaches a canonical term . Second, it applies to join terms and to condense the remaining contracts.
[TABLE]
5.8 Weak Blame-preservation
While reorganizing contracts, the Subset Transformation did no strictly preserve the blame behaviour of a program. An ill-behaved program by lead to another contract violation first, whereas well-behaved programs still result in the same output.
Conjecture 2** (Weak Blame-preservation).**
For all it hold that either and or and .
6 Technical Results
In addition to weak and string blame preservation, our contract simplification grantees not to introduce more predicate checks at run time. Even throut we reorganize and duplicate contract assertions, the total number of predicate checks at run time remains the same or decrease on every transformation step.
Definition 6** (Size).**
The size of a closed term is the number of predicates checks during reduction of .
Theorem 1** (Improvement).**
For each term with it holds that .
Finally, to prove soundness of our static contract simplification, we need to show that our transformation terminates.
Theorem 2** (Termination).**
For each term , there exists a canonical term such that .
7 Practical Evaluation
To give an insight into the run time improvements of our system we apply the simplifications to different versions of the addOne example from Section 2. Our testing procedure uses the addOne function to increase a counter on each iteration in a while loop.
Each example program addresses a certain property and contains a different number of contracts. For example, Example2 corresponds the addOne function in Section 2.1 and Example4 corresponds to the function in Section 2.6. Appendix J shows the JavaScript implementation of all benchmark programs.
To run the examples we use the TreatJS Keil and Thiemann [2015b] contract system for JavaScript and the SpiderMonkey333https://developer.mozilla.org/en-US/docs/Mozilla/Projects/SpiderMonkey JavaScript engine. Lacking an implementation (beyond the PLT Redex model) we applied the simplification steps manually.
Figure 16 shows the execution time required for a loop with 100000 iterations. The numbers indicate that the Baseline Simplification improves the run time by approximately 28%, whereas the Subset Simplification makes an improvement up to 62%. Appendix J shows the full table of results.
In addition, there is another aspects not already addressed by Keil and Thiemann [2015b]: Adding contracts may also prevent a program from being optimized. The SpiderMonkey engine, for example, uses two different optimizing compilers to speed up operation. When activating SpiderMonkey’s optimizing JIT, the run time of the normal program without contracts decreases by 20x, whereas the run time of the program with contracts only decreases by 2x. This lack of optimization opportunities for the JIT is one important reason for the big run time deterioration they reported.
8 Related Work
Higher-Order Contracts
Software contracts were introduced with Meyer’s Design by Contract™ methodology Meyer [1988] which stipulates the specification of Hoare-like pre- and postconditions for all components of a program and introduces the idea of monitoring these contracts while the program executes.
Findler and Felleisen [2002] extend contracts and contract monitoring to higher-order functional languages. Their work has attracted a plethora of follow-up works that ranges from semantic investigations Blume and McAllester [2006]; Findler and Blume [2006] over studies on blame assignment Dimoulas et al. [2011]; Wadler and Findler [2009] to extensions in various directions: intersection and union contracts Keil and Thiemann [2015a], polymorphic contracts Ahmed et al. [2011]; Belo et al. [2011], behavioral and temporal contracts Dimoulas et al. [2012]; Disney et al. [2011], etc.
Contract Validation
Contracts may be validated statically or dynamically. However, most frameworks perform run-time monitoring as proposed in Meyer’s work.
Dynamic contract checking, as for example performed by Findler and Felleisen [2002]; Keil and Thiemann [2015b], enable programmers to specify properties of a component without restricting the flexibility of the underlying dynamic programming language. However, run time monitoring imposes a significant overhead as it extends the original program with contract checks.
Purely static frameworks (e.g., ESC/Java Flanagan et al. [2002]) transform specifications and programs into verification conditions to be verified by a theorem prover. Others Xu et al. [2009]; Tobin-Hochstadt and Van Horn [2012] rely on program transformation and symbolic execution to prove adherence to contracts.
Static contract checking avoids additional run-time checks, but existing approaches are incomplete and limited to check a restricted set of properties. They rely on theorem proving engines to discharge contracts that are written in the host language: the translation to logic may not always succeed.
Contract Simplification
Nguyen et al. [2014] present a static contract checker that has evolved from Tobin-Hochstadt and Van Horn’s work on symbolic execution Tobin-Hochstadt and Horn [2012]. Their approach is to verify contracts by executing programs on unknown abstract values that are refined by contracts as they are applied. If a function meets its obligation, the corresponding contract gets removed. However, their approach only applies to the positive side of a function contract.
Propagating contracts is closely related to symbolic executions. Both refine the value of a term based on contracts, whether by moving the contract through the term or by using an abstract value.
Compared to our work, Nguyen et al. [2014] addresses the opposite direction. Where we unroll a contract to its enclosing context and decompose a contract into its components, they verify the function’s obligations based on the given domain specification. However, in case the given contract cannot be verified, they must retain the whole contract at its original position and they are not able to simplify the domain portion of a function contract.
Furthermore, their symbolic verification is not able to handle true alternatives in the style of intersection and union contracts.
We claim that both approaches are complementary to one another. Our contract simplification would benefit from a preceding verification that simplifies the function’s obligations before unrolling a contract to the enclosing context.
Xu [2012] also combines static and dynamic contract checking. Her approach translates contracts into verification conditions that get verified statically. Whereas satisfied conditions will be removed, there may be conditions that cannot be proved: they remain in the source program in the form of dynamic checks.
9 Conclusion
The goal of static contract simplification is to reduce the overhead of run-time contract checking. To this end, we decompose contracts and propagates their components through the program. In many cases we are able to discharge parts of contracts statically. The remaining components are simplified and reassembled to a new and cheaper contract at a module boundary.
As a novel aspect, we can simplify contracts that cannot be verified entirely at compile time. The remaining contract fragments stay in the program and get lifted to the enclosing module boundary.
A case study with microbenchmarks shows some promise. Our simplification decreases the total number of predicate checks at run time and thus reduces the run-time impact caused by contracts and contract monitoring. The study also shows that the degree of improvement depends on the granularity of contracts. Fine-grained contracts enable more improvement.
Appendix A Constraint Satisfaction
The dynamics in Figure 3 use constraints to create a structure for computing positive and negative blame according to the semantics of subject and context satisfaction, respectively. To this end, each blame identifier is associated with two truth values, and . Intuitively, if is false, then the contract is not subject-satisfied and may lead to positive blame for . If is false, then there is a context that does not respect contract and may lead to negative blame for .
An interpretation of a constraint list is a mapping from blame identifiers to records of elements of , such that all constraints are satisfied. We order truth values by and write for the reflexive closure of that ordering. This ordering reflects gathering of informations with each execution step.
Formally, we specify the mapping by
[TABLE]
where ranges over metavariable and constraint satisfaction by a relation , which is specified in Figure 18.
In the premisses, the rules apply a constraint mapping to boolean expressions over constraint variables. This application stands for the obvious homomorphic extension of the mapping.
Every mapping satisfies the empty list of constraints (CS-Empty). The concatenation of a constraint with a constraint list corresponds to the intersection of sets of solutions (CS-State). The indirection constraint just forwards its referent (CT-Indirection).
In rule Ct-Flat, is the outcome of the predicate of a flat contract. The rule sets subject satisfaction to false if and otherwise to true, where the function translates values to truth values by stripping delayed contracts (see Figure 17). A flat contract never blames its context so that is always true.
The rule CT-Function determines the blame assignment for a function contract from the blame assignment for the argument and result contracts, which are available through and . Let’s first consider the subject part. A function satisfies contract if it satisfies its obligations towards its argument and if the argument satisfies its contract then the result satisfies its contract, too. The first part arises if the function is a higher-order function, which may pass illegal arguments to its function-arguments. The second part is partial correctness of the function with respect to its contract.
A function’s context (caller) satisfies the contract if it passes an argument that satisfies contract and uses the result according to its contract . The second part becomes non-trivial with functions that return functions.
The rule CT-Intersection determines the blame assignment for an intersection contract at from its constituents at and . A subject satisfies an intersection contract if it satisfies both constituent contracts: . A context, however, has the choice to fulfill one of the constituent contracts: .
Dually, the rule Ct-Union determines the blame assignment for a union contract at from its constituents at and . A subject satisfies a union contract if it satisfies one of the constituent contracts: . A context, however, needs to fulfill both constituent contracts: , because it does not know which contract is satisfied by the subject.
Appendix B Canonical Terms
Canonical (non-transformable) terms are the output of our transformation. Each level has its own output grammar consisting of term that cannot be further transformed at this level.
Canonical terms distinguish contract-free term (indicated by latter ) from terms with a contract (indicated by latter ).
B.1 Canonical Term of the Baseline Transformation
This sections considers the output terms of the Baseline Transformation (Section 4.3). Figure 19 defines the syntax of canonical terms and as a subset of term .
A terms without a contract is either a value term , including first-order constants and lambda abstractions, or a non-value term , which is either a variable, a blame term, an application, a primitive operation, or a condition.
Applications are divided into different combinations. This excludes all reducible combinations and only the given terms remain. For example, a function contract on the left side of an application is reducible, whereas a function contract in the right side is only reducible if the left side is a lambda term.
A canonical term is a term , which is either a term or a term with an indefinite number of delayed contracts on the outermost position. Terms are all values with remaining contracts. Terms are all terms with immediate contracts or contracts on the outermost position. As all immediate contracts on values will be reduced, immediate contracts only remain on non-value terms .
In addition to the canonical terms, Figure 19 shows the syntax of transformable (non-canonical) terms , which is the complement of the canonical terms .
A non-canonical term is either a term that contains a non-canonical term or one of the patterns addressed by our transformation rules in Section 4.3.
Lemma 5** (Terms).**
For all terms it holds that is either a canonical term or a transformable (non-canonical) term .
B.2 Canonical Term of the Subset Transformation
Figure 20 shows the definition of canonical term and source terms as a restriction of the already defined canonical terms. For readability, we reuse the same symbols as in Section LABEL:sec:appendix/baseline/terms. The repeatedly defined terms replace the already existing definition, whereas every other definition remains valid.
A lambda abstractions now did not contain immediate contracts on its argument and terms only contain contracts that are not subsumed by another contract on that term. Terms now contains a blame terms with a remaining contract.
Lemma 6** (Terms).**
For all terms it holds that is either a canonical term or a transformable (non-canonical) term .
Appendix C Auxiliary Functions and Definitions
This section shows some auxiliary functions and definitions used in the paper.
C.1 Function
Each top-level contract assertion is rooted in one blame label , i.e. for every blame identifier there exists a path from to a blame label .
To computer the root label for an identifier we need to walk backwards through all constraints on a path until we reach the top level blame label .
To do so, Figure 21 introduces a constraint context , which is either a hole or constraint extending a constraint context .
Figure 22 finally shows the computation of function .
C.2 Sign of a Blame Identifier
Following the definition in Section 3, constraints implement a tree rooted in a blame label . Within the tree every blame identifier can report positive or negative blame, depending on its constraint when mapping one of its truth values ( or ) to false.
Thus, we define the sign of a blame identifier as the responsibility to satisfy the subject part in this identifier . We represent signs by blame term B that would result from a subject blame in .
Definition 7**.**
B* is the sign of a blame identifier in if leads to on a single path for any .*
In this case, every alternative must be treated as neutral, i.e. they do not stop or change the arising blame. Thus we consider only a single path from to its root .
To compute the sign of a blame identifier , Figure 23 first defines an inversion of blame terms B that flips the responsibility. Figure 24 than shows the computation of the sign of blame identifier . It is defined by induction and tracks swapping of responsibilities on function and inversion constraints.
C.3 Computation of Blame Terms
To computes a blame term resulting from a predicate violation () in we need to compute the sign of in and to annotate the resulting blame term with the root blame identifier of in .
[TABLE]
C.4 Compute joined Assertion Context
We define the join of two assertion contexts and by
[TABLE]
Term computes a new context with assertions from that are not already contained in . Its computation is defined as:
[TABLE]
We write to indicate that the assertion of under blame label and blame variable is contained in , and for its negation. Contract entailment is defined by:
[TABLE]
Appendix D Picky Semantics
The semantics in Section 4 guarantee Strong Blame-preservation with respect to Lax evaluation semantics (cf. Section 3.5). Lax unpacks contracts from values that flow to a predicate, i.e. a contract cannot violate another contract.
The Baseline Transformation makes this intuitively when processing the rule Push/Immediate. It pushes a delayed contract out of an assertion with an immediate contract, such that the predicate will not see the delayed contract. This step is entirely required for following transformation steps.
When considering Picky (or even Indy) evaluation semantics, a contract must remain on a value when the value is used in a predicate. Consequently, we cannot pushes a delayed contract out of an assertion with an immediate contract without changing the blame behaviour of the underlying program.
To enables Picky (or Indy) semantics, rule Push/Immediate (Figure 8) must be replayed by another rule that unrolls a delayed contract in an immediate contract when pushing the delayed contract. Figure 25 shows the new rule.
Here, term is a new intermediate term that unrolls a delayed contract in a predicate (cf. rule Unroll). Figure 26 shows its semantics.
Rule Extend/Predicate unrolls a delayed contract to all uses of the value in a predicate and rule Extend/Predicate proceeds on the unchanged predicate in case that the predicate is not a lambda abstraction.
Indeed, it would also be possible to replace predicate by as it enforces when the predicate is used in an application. However, unrolling the contract enables to apply further simplification steps in the function’s body.
Appendix E Proofs of Theorems
E.1 Proof of Lemma 1
Proof of Lemma 1.
Immediate from the definition of canonical and non-canonical terms (Section B.1). ∎
E.2 Proof of Lemma 4
Proof of Lemma 4.
is an equivalence relation if and only if it is reflexive, symmetric, and transitive. Proof by induction over . ∎
E.3 Proof of Conjecture 1
E.4 Congruence of States and Terms
Definition 8**.**
Two configurations and are structural equivalent under renaming , written with iff with .
Lemma 7**.**
For all configurations and with it holds that and with .
Proof of Theorem 7.
Proof by induction over and . ∎
E.5 Congruence of States and Terms
Definition 9**.**
State is an effect-free extension of state , written , iff and with .
Lemma 8**.**
For terms , states , and transformations it hold that .
Proof of Theorem 7.
Immediate by the definition of and . Every new constrains is composed of fresh blame variable . Proof by induction over . ∎
Proof Sketch for Conjecture 1.
Let reduction output . For all terms and states with it hold that and with .
As our transformation only propagates contract assertions and did not modify the underlying program, we know that if and then .
To prove preservation, we show that the transformed term results in the same reduction sequence than the original term and that the both, state and terms, are equivalent under variable renaming .
Proof by induction over .
Rule Unfold/Assert:
, , and .
- (1)
From and it follows that and by rule Assert it follows that . 2. (2)
From lemma 7 it follows the with .
Claim holds because with .
Rule Unfold/Union:
Equivalent to case Unfold/Assert.
Rule Unfold/Intersection:
Equivalent to case Unfold/Assert.
Rule Unfold/D-Function:
, , and .
- (1)
From and it follows that and . By rule D-Function it follows that . 2. (2)
From lemma 7, and it follows that and with .
Claim holds because with .
Rule Unfold/D-Intersection:
Equivalent to case Unfold/D-Function.
Rule Unroll:
Immediate from rule Beta.
Rule Lower:
Immediate from rule D-Function.
Rule Push/Immediate:
Immediate from rule Flat.
Rule Push/False:
Immediate from rule Flat.
Rule Push/If:
Immediate from rules True and False.
Rule Convert/True:
Immediate from rule Unit.
∎
E.6 Proof of Lemma 2
Proof of Lemma 2.
is a preorder if and only if it is reflexive and transitive. Proof by induction over . ∎
E.7 Proof of Lemma 3
Proof of Lemma 3.
Immediate from the definition of canonical and non-canonical terms (Section B.2). ∎
E.8 Proof of Conjecture 2
Proof Sketch for Conjecture 2.
Equivalent to proof of Conjecture 1. However, certain rules change the order of contract checks. So wen need to consider two cases: one where the early contract is satisfied, and one where it is violated. ∎
E.9 Proof of Theorem 1
Proof of Theorem 1.
Proof by induction over . It is immediate from the definition that all rules, expect rule Unroll, either decompose, eliminate, or graft a contract. It remains to shows that:
no rules duplicates contract checks, and 2. 2.
no rule pushes contract checks from one function body (or branch in a condition) to the enclosing body.
Rule Unroll
. This rule grafts the assertion of a delayed contract to all uses of the contracted value. From , we have that for all first and by rule Beta it follows that reduces to . By rule Unroll we have that translates to . From , we now have that and by rule Beta if follows that , which is equivalent to the result of the original reduction.
Rule Lift
. This rule lifts an immediate contract nested in a function body to a new function contract. However, this contract never applies if the function is not executed. Thus, it preserves the number contract checks.
Rule Lower
. This rule lowers a contract to the function boundary. But, this contract never applies if the function is not executed. It also preserves the number contract checks.
Rule Push/If
. This rule pushes an immediate contract out of a condition, if the contract definitely applies to both branches. Thus, it preserves the number contract checks.
Otherwise
Every other rule either decomposes or eliminates a contract, or reverses the order of contract checks. Thus they reduces or preserves the total number contract checks at run time.
∎
Proof of Theorem 2.
The transformation terminates with a canonical term because
(1) there are no cycles and
(2) there is no transformation step that introduces new contract check.
All rules, except rule Unroll, decompose or eliminate a contract, or grafts a contract to an enclosing term. Only rule Unroll duplicates a contract to all uses of the contracted value. However, as the transformation did not lift delayed contracts, it is not a cycle. 2. 2.
Immediate from Theorem 1.
∎
Appendix F Simplify Intersection and Union
Apart from the subset optimization, which reduces a contract assertion based on more restrictive assertion, we can also use the subcontract relation to simplify contracts before unfolding.
For example, the intersection contract Positive*? Natural? Natural? Positive?* can be simplified to a single function contract Positive*? Positive?*. This is because, the context can choose to call the function with a natural or positive number. However, in case the input is a natural number, but not a positive number, than the range must be a positive number. And, in case the input is a positive number, than it is also a natural number (as positive numbers are a proper subset of natural numbers) and thus the output needs to satisfy both range contract, i.e. it must be a positive number.
So, we can simplify the intersection because Natural*? Positive?* is an ordinary subset of Positive*? Natural?* (cf. Section 5.2). Its domain is less or equal restrictive and its range is more or equal restrictive.
In general, we can simplify intersection and union contracts if one operand is an ordinary subset of the other operand. Figure 27 shows some simplification rules that omits one branch of an alternative if that alternative is subsumed by the other branch.
To keep the system deterministic, we must simplify contracts at assertion time and thus we skip rule Unfold/Assert in this cases.
Appendix G Introducing new Success Contracts
Our core rules in Section 4 and Section 5 follows the overall guideline not to approximate contract violations. However, developers are free to choose a higher degree of optimization, while over-approximating contract failures at compile time and introducing new module boundaries.
This level’s rules create some kind of success contracts by over-approximating contracts and by lifting contracts to the upper-most boundary. However, this is not a real optimization as it might lift checks that never happen at run time.
Figure 28 defines the syntax of our canonical terms as a subset of term , and Figure 29 shows possible transformation.
Rule Lift lifts every contract on an argument . This step over-approximates contract violations as it also lifts contracts nested in conditions and function applications that might never apply.
Rule Blame immediately updates the constraint state with information about a failing contract. This might result in a blame state, even if the ill behaved term is never executed.
Finally, the rule Subset lifts to the Subset Reduction and rule Trace unpacks parallel observation. Obviously, rule Blame replaces the rule with the same name in and we are never allowed to unroll a once lifted contract. Otherwise we would end up in a cycle.
Appendix H Propagating Blame
In the preceding example we have seen that all contracts of a failing alternative can be removed and only one must remain on the first failing term. As we split alternatives in different observation where every contract must be fulfilled, we can report a violation for that branch immediately when observing a violation. Every other contract can be ignored as this branch definitely runs into an error.
However, this is not completely true. We are only allowed to remove contracts in the same context as the violation occurs. We cannot treat a contract as violated if the violation only occurs in a certain aspect of the program.
For example, consider the following source program.
After applying some simplification steps, we obtain the following intermediate term.
Even though we do not know that addOne violates the contract on plus, we are not allowed treat the contract as violated because we do not know if addOne is ever executed. But, we can replace addOne’s body by a blame term that reports a violation whenever the function is executed. In addition, a remains on the functions body.
Having a blame term and seems to be twofold, but can be lowerd to a new function contract on addOne, which is than unrolled to all places where addOne is used, as the following example demonstrates.
Now, the same transformation steps apply as for normal contract. The function contract gets unrolled, whereby gets asserted to another term. If it so happens the next function body gets transformed to a blame term with a remaining .
Continuing in this way propagates the information of a failing contact through applications and conditions until it reaches the outermost boundary. Within this boundary we definitely run into a contract violation. The following example shows the result.
Appendix I An Evaluation of Contract Monitoring
Dynamic contract checking impacts the execution time. Source of this impact is
(1) that every contract extents the original source with additional checks that need to checked when the program executes and
(2) that the contract monitor itself causes some runtime overhead.
To demonstrate, we consider runtime values obtained from the TreatJS contract framework for JavaScript Keil and Thiemann [2015b]. To the best of our knowledge, TreatJS is the contract framework with the heaviest runtime deterioration. Reason for this is its flexibility and its support for full intersection and union contracts Keil and Thiemann [2015a]. The presence of intersection and union contracts require that a failing contract must not signal a violation immediately. As a violation depends on combinations of failures in different sub-contracts the contract monitor muss continue even if a first error occurs and connect the outcome of each sub-contract with the enclosing operations.
To evaluate the runtime deterioration, they applied there framework to benchmark programs from the Google Octane 2.0 Benchmark Suite444https://developers.google.com/octane/. The benchmark programs measure a JavaScript engine’s performance by running a selection of complex and demanding programs.
For testing, they inferred a function contract for every function expression contained a program and assert the function contract when the program executes.
Figure 30 contains the runtime values of all benchmark programs in two configurations, which are explained in the figure’s caption. As expected, all run times increase when adding contracts.
The examples show that the run-time impact of contract monitor depends on the program and on the particular value that is monitored. While some programs like Richards, DeltaBlue, RayTrace, and Splay are heavily affected, others are almost unaffected: Crypto, NavierStokes, and Mandreel, for instance.
It follows that the impact of a contract depends on the frequency of its application. A contract on a heavily used function (e.g., in Richards, DeltaBlue, or Splay) causes a significantly higher deterioration of the run-time.
For better understanding, Figure 31 lists some numbers of internal counters. The numbers indicate that the heavily affected benchmarks (Richards, DeltaBlue, RayTrace, Splay) contain a very large number of predicate checks. Other benchmarks are either not affected (RegExp, zlib) or only slightly affected (Crypto, pdf.js, Mandreel) by contracts.
For example, the Richards benchmark performs 24 top-level contract assertions (this are all unique contracts in a source program), 1.6 billion internal contract assertions (including top-level assertions, delayed contract checking, and predicate evaluation), and 936 million predicate evaluation.
To sum up, we see that number of predicate checks is substantially responsible for the runtime deterioration of a contract system. Thus, reducing the number of predicate checks will entirely improve the runtime.
Appendix J Practical Evaluation, continued
To demonstrate the run time improvement we applied our contract simplification to a number simple examples, as introduces in Section 2 and Section 7. The testing procedure is a simple while loop that uses different versions of an addOne function to increase a counter on every iteration.
This section shows the examples programs written in JavaScript and the full table of results. To run the examples we use the TreatJS555 https://github.com/keil/TreatJS Keil and Thiemann [2015b] contract system for JavaScript and the Mozilla SpiderMonkey666 https://developer.mozilla.org/en-US/docs/Mozilla/Projects/SpiderMonkey engine. While there is actually no implementation of our transformation system for JavaScript, we applied all transformation manually and produces the simplified contracts by hand.
In TreatJS, function assert asserts a contrat (given as second argument) to a subject value (given as first argument). Constructor AFunction creates a function contract from a set of argument contracts (given as first argument) and a return contract (given as second argument). Constructor Intersection creates an intersection contract from two other contracts. _Number, _Natural, _Positive, _Negative, _String are flat contrasts checking for number values, natural numbers, positive numbers, negative numbers, and string values, respectively.
J.1 The example programs
Example 1** (addOne1).**
In a first example we add a simple function contract to plus restricting its domain and range to number values. Every use of addOne1 triggers three predicates checks.
Example 2** (addOne2).**
Our second example adds an intersection contract to plus. As the native + operator is overload and works for strings and numbers, our contract restricts the domain either to string or number values and ensures that the function has to return a string or a number value corresponding to the input. Every use of addOne2 triggers six predicate checks.
Example 3** (addOne3).**
The third example extends addOne1 by adding another function contract to addOne. The contract restricts addOne’s domain to natural numbers and requires a positive number as return. In combination, every use of addOne3 triggers 5 predicate checks.
Example 4** (addOne4).**
The next example merges the intersection contract on plus (from Example 2) and the contract on addOne (Example 3). Every call of addOne4 leads to a total number 8 predicate checks.
Example 5** (addOne5).**
In this example we also overload addOne by making either string concatenation or addition, depending on addOne’s input. While adding an intersection contract to addOne, every use of addOne5 leads to 10 predicate checks.
Example 6** (addOne6).**
Our last example simulates the case that we add fine-grained properties to plus and addOne. In this case we state different properties in different function contracts and use intersections to combine those properties. Before simplifying the contract, every call of addOne6 leads to a total number 17 predicate checks.
J.2 The Run-Time Improvements
Figure 32 finally contains the execution time and the number of predicate checks during execution of all examples programs in different configuration, as explained in the figures caption.
In addition to the examples from Section J.1, it also contains the run time of the addOne program without contracts, and the run time of the addOne example where we only wrap the functions in a proxy, but did not apply any contracts.
To sum up, the the Baseline Simplification improves the run time by approximately 28%, whereas the Subset Simplification makes an improvement by approximately 58.68%. Clearly, the improvement strictly depends on the granularly of predicates and contracts.
The numbers also indicate that the run time improvements remain identical, whether we use an optimizing compiler or not. But, deactivating the optimizing compiler increases the run time of the program without contracts by factor 4.83 (No-Ion) and by factor 20.17 (No-Jit), whereas the version with contracts increases only by factor 1.5 (No-Ion) and factor 2.09 (No-Jit).
The numbers also shows that adding contracts, even without any functionality, increases the run time by factor 71.2 (Full), factor 13.7 (No-Ion), and factor 5 (No-Jit).
This illustrates that contracts prevent a program from being optimized efficiently by an optimizing compiler.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1Ahmed et al. [2011] A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame for all. In Ball and Sagiv [ 2011 ] , pages 201–214.
- 2Ball and Sagiv [2011] T. Ball and M. Sagiv, editors. Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011 , 2011. ACM.
- 3Belo et al. [2011] J. F. Belo, M. Greenberg, A. Igarashi, and B. C. Pierce. Polymorphic contracts. In G. Barthe, editor, Proceedings of the 20th European Symposium on Programming , volume 6602 of Lecture Notes in Computer Science , pages 18–37, Saarbrücken, Germany, Mar. 2011. Springer-Verlag. ISBN 978-3-642-19717-8.
- 4Blume and Mc Allester [2006] M. Blume and D. Mc Allester. Sound and complete models of contracts. Journal of Functional Programming , 16:375–414, July 2006. ISSN 0956-7968. 10.1017/S 0956796806005971 . · doi ↗
- 5Dimoulas et al. [2011] C. Dimoulas, R. B. Findler, C. Flanagan, and M. Felleisen. Correct blame for contracts: No more scapegoating. In Ball and Sagiv [ 2011 ] , pages 215–226.
- 6Dimoulas et al. [2012] C. Dimoulas, S. Tobin-Hochstadt, and M. Felleisen. Complete monitors for behavioral contracts. In European Symposium on Programming , volume 7211 of Lecture Notes in Computer Science , Tallinn, Estland, Apr. 2012. Springer-Verlag.
- 7Disney [2013] T. Disney. contracts.js. https://github.com/disnet/contracts.js , Apr. 2013.
- 8Disney et al. [2011] T. Disney, C. Flanagan, and J. Mc Carthy. Temporal higher-order contracts. In O. Danvy, editor, Proceedings International Conference on Functional Programming 2011 , pages 176–188, Tokyo, Japan, Sept. 2011. ACM Press, New York. ISBN 978-1-4503-0865-6.