Default Predicates for Omitted Clauses Sample Clauses

Default Predicates for Omitted Clauses. All clauses of a change contract do not have to be specified, as mentioned in Section 3.1. Default predicates are used for omitted clauses, following the rule described in Table I. ∧ ∧ If an ensures (or a signals) clause is omitted, ensures true (or signals true) is used by default. To understand why true is used as a default clause for an ensures clause, recall that, given a full change contract (true, ψ,θ ; true,ψr,θ r),4 our change contract inference rule in Figure 5(d) checks whether change condition ψr θ r holds at the end of the updated version whenever update condition ψ θ holds at the end of the previous version. When omitting the predicate ψr of the ensures clause and only the predicate θ r of the signals clause is used, the change condition we want to check is true θ r. Thus the omitted predicate ψr should be true. Similarly, the default predicate of an omitted signals clause should be true. \ \ \ Meanwhile, when omitting the predicate ψ of the when ensured clause, the default value of ψ seems to be false at first, considering the update condition ψ θ . However, the problem is that one can omit both when ensured and when signaled clauses simul- taneously, as in the following change contract: ensures result== prev( result)+1, which describes the expectation that the return value of the updated version should be one larger than the return value of the previous version. If this is the case, the use of false as a default predicate makes the update condition false and, as a result, the change condition is not checked. To avoid such situations, we assign a default predicate dif- ferently depending on the context. If it is the case that only either of the when ensured or when signaled clause is omitted, we use false as a default predicate for the omitted clause. However, if both when ensured and when signaled clauses are omitted, we use true as a default predicate instead. 4For simplicity of the description, we give true to the when required and requires clauses. ACM Transactions on Software Engineering and Methodology, Vol. 24, No. 3, Article 18, Pub. date: May 2015. Software Change Contracts 18:13 Lastly, let us explain the case for when required. If there are no structural changes, it is most likely that writers of a change contract would want to assume the same precondition for the previous and the updated versions. We accordingly assign the predicate of a given requires clause to the omitted when required clause.