Submitted by Nayara Passos (nayara.passos@ufpe.br) on 2015-03-12T12:46:58Z
No. of bitstreams: 2
TESE Henrique Emanuel Rabêlo.pdf: 2393775 bytes, checksum: b74f8b8b1b46d5879b334348c3110846 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T12:53:22Z (GMT) No. of bitstreams: 2
TESE Henrique Emanuel Rabêlo.pdf: 2393775 bytes, checksum: b74f8b8b1b46d5879b334348c3110846 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T12:53:22Z (GMT). No. of bitstreams: 2
TESE Henrique Emanuel Rabêlo.pdf: 2393775 bytes, checksum: b74f8b8b1b46d5879b334348c3110846 (MD5)
license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5)
Previous issue date: 2014 / 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. / 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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufpe.br:123456789/12354 |
| Date | 31 January 2014 |
| Creators | Rebêlo, Henrique Emanuel Mostaert |
| Contributors | Lima, Ricardo Massa Ferreira de |
| Publisher | Universidade Federal de Pernambuco |
| Source Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UFPE, instname:Universidade Federal de Pernambuco, instacron:UFPE |
| Rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil, http://creativecommons.org/licenses/by-nc-nd/3.0/br/, info:eu-repo/semantics/openAccess |
Page generated in 0.0032 seconds