CHANGE CONTRACT LANGUAGE Clause Samples

CHANGE CONTRACT LANGUAGE. To express intended program changes, we extend a subset of JML [▇▇▇▇▇ et al. 2005], the de facto lingua franca when giving checkable formal specifications to Java pro- grams. In fact, one of our goals in designing a change contract language is to be as close to an existing popular specification language as possible to lower the learning bar- rier, and our syntactic extension to JML is very limited. However, JML (or any other specification languages), to the best of our knowledge, is not expressive enough to ex- press program changes across two consecutive versions, and this requires to propose nontrivial semantic extensions. Notes on Expressivity. While the main objective of our change contract language is to specify behavioral changes that occur between two consecutive versions of a method, it is also possible to specify with this language accompanying structural changes such as adding/deleting method parameters or fields. While our change contract language captures the relationship among program variable values at the input/output points of the previous/updated program versions, it is not powerful enough to express temporal properties of changes in variable values, as in temporal logics. Lastly, as in JML, we are concerned only with sequential Java programs and do not consider multithreading. A change contract is specified above the signature of a method m as an annotation between “/*@ changed behavior” and “@*/”. We call such a method m the target method of a given change contract. We require that expressions used in a change contract, including method calls, must be free of side-effects and exceptions. Also, their execution must terminate. A change contract is maintained as a contract file (e.g., XXX.scc) separated from Java files.