Contract modularity in design by contract languages

Abstract

Design by Contract (DbC) is a popular technique for developing programs using behavioral specifications. In this context, researchers have found that the realization of DbC is crosscutting and fares better when modularized by Aspect-Oriented Programming. However, previous efforts aimed at supporting crosscutting contracts modularly actually compromised the main DbC principles. For example, in AspectJ-style, reasoning about the correctness of a method call may require a whole-program analysis to determine which advice applies and what that advice does relative to DbC implementation and checking. Also, when contracts are separated from classes a programmer may not know about them and may break them inadvertently. Unlike an AspectJ-like language, a DbC language keeps the main DbC principles such as modular reasoning and documentation. However, a recurrent pre- or postcondition specification remains scattered across several methods in many types. Unfortunately, this is not the only modularity problem we have with existing DbC languages. Such languages along with their respective runtime assertion checkers are inconsistent with information hiding rules because they check specifications in an overly-dynamic manner on the supplier side. This implies that during error reporting, hidden implementation details are exposed to non-privileged clients. Such details should not be used in a client’s correctness proof, since otherwise the proof would be invalidated when they change. Therefore, if programmers have carefully chosen to hide those parts “most likely” to change, most changes, in the hidden implementation details, do not affect either module clients nor DbC error reporting. In this work we solve these problems with AspectJML, a new specification language that supports crosscutting contracts for Java code. We also show how AspectJML supports the main DbC principles of modular reasoning and contracts as documentation. Additionally, we explain how AspectJML combined with our client-aware checking technique allows runtime checking to use the privacy information in specifications, which promotes information hiding. We use JML for concreteness, but the solution we propose can also be used for other Java-like languages and their respective DbC languages. To conclude, we conduct an evaluation to assess the crosscutting contract modularization using AspectJML, where we observe that its use reduces the overall design by contract code, including pre- and postconditions, but introduces a small overhead during compile time and can increase the resulting bytecode due to code instrumentation to check ordinary and crosscutting contracts

Design by Contract (DbC) ´e uma t´ecnica popular para desenvolvimento de programas usando especifica¸c˜oes comportamentais. Neste contexto, pesquisadores descobriram que a implementao de DbC ´e crosscutting e, portanto, sua implementa¸c˜ao ´e melhor modularizada por meio da Programa¸c˜ao Orientada a Aspectos (POA) por´em, os mecanismos de POA para dar suporte a modularide de contratos, de fato comprometem sua modularidade e entendidmento. Por exemplo, na linguagem POA AspectJ, o racioc´ınio da corretude de uma chamada de m´etodo requer uma an´alise global do programa para determinar quais advice aplicam e sobretudo o que esses advice fazem em rela¸c˜ao a implementa ¸c˜ao e checagem DbC. Al´em disso, quando os contratos so separados das classes o programador corre o risco de quebrar-los inadvertidamente. Diferentemente de uma linguagem POA como AspectJ, uma linguagem DbC preserva as principais caractersticas DbC como raciocnio modular e documenta¸c˜ao. No entanto, pr´e- e p´os-condi¸c˜oes recorrentes continuam espalhadas por todo o sistema. Infelizmente esse n˜ao o ´unico problema relacionado com modularidade que temos em linguagens DbC existentes, o seu com respectivos verificadores dinˆamicos so inconsistentes com as regras de information hiding devido a naturaze overly-dynamic na qual os contratos s˜ao checados no lado servidor. Este problema implica que durante a reportagem de erros, detalhes de implementa¸c˜ao so expostos para clientes no privilegiados. Portanto, se os programadores cuidadosamente escolherem as partes que devem ser escondidas dos clientes, durante a checagem dinˆamica de contratos, as mudanas nessas partes n˜ao deveriam afetar nem os clientes dos m´odulos nem a reportagem de erros de contratos. Neste trabalho n´os resolvemos esses problemas com AspectJML, uma nova liguagem de especifica¸c˜ao que suporta contratos crosscutting para c´odigo Java. Al´em disso, n´os demonstramos como AspectJML usa as principais caractersticas de uma linguagem DbC como racioc´ınio modular e documenta¸c˜ao dos contratos. Mais ainda, n´os mostramos como AspectJML combinado com nossa t´ecnica chamada de client-aware checking permite uma checagem dinˆamica de contratos que respeitem os princ´ıpios de information hiding em especifica¸c˜oes. Neste trabalho usamos JML para fins concretos, mas nossa solu¸c˜ao pode ser utilizadas para outras linguagems Java-likee suas respectivas linguagens DbC. Para concluir, n´os conduzimos uma avalia¸c˜ao da nossa modulariza¸c˜ao dos contratos crosscutting usando AspectJML, onde observamos que seu uso reduz o esforo de escrever pr´e- e p´os-condies, por´em com um pequeno overhead em tempo de compila¸c˜ao e instrumentação de código para checagem de contratos.