Refactoring as formal refinements

• Ano de defesa: 2004
• Autor(a) principal: Lopes Cornélio, Márcio
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Pernambuco
• Palavras-chave em Português: Métodos Formais, Cálculo de refinamentos, Orientação a objet
• Link de acesso: https://repositorio.ufpe.br/handle/123456789/1891

A reestruturação de programas no contexto da orientação a objeto é também conhecida como refactoring e consiste em mudanças na estrutura interna de um software, sem modificar seu com portamento externo, a ¯m de melhorar sua legibilidade e torn¶a-lo mais f¶acil de passar por futuras mudan»cas. Na pr¶atica, refactoring baseia-se em compila»c~ao e testes para assegurar a preserva»c~ao do comportamento. Trabalhos como os de Opdyke e Roberts foram realizados com vistas µa formaliza»c~ao de refac- torings por meio da identi¯ca»c~ao de condi»c~oes que devem ser satisfeitas para assegurar que uma mudan»ca num programa preserva o comportamento do mesmo. As condi»c~oes, geralmente escritas na linguagem do c¶alculo de predicados, s~ao introduzidas como pr¶e e p¶os-condi»c~oes dos refactor- ings. Outras abordagens para a prova de preserva»c~ao do comportamento de refactorings usam formalismos como an¶alise conceitual e reescritura de grafos. Contudo, n~ao h¶a t¶ecnica alg¶ebrica que apresente refactorings como transforma»c~oes que preservam o comportamento, com prova deste fato. Nossa principal contribui»c~ao constitui-se na apresenta»c~ao de refactorings como transforma»c~oes de programas escritos em rool (Re¯nement object-oriented Language), uma linguagem baseada em Java, com classes, controle de visibilidade, liga»c~ao din^amica, e recurs~ao. A linguagem rool permite que raciocinemos sobre programas orientados a objetos e especi¯ca»c~oes, pois a mesma une estas constru»c~oes como no c¶alculo de re¯namentos de Morgan. A sem^antica de rool ¶e baseada em weakest preconditions. Um conjunto de leis de programa»c~ao est¶a dispon¶³vel tanto para os comandos imperativos de rool quanto para construtores relacionados µa orienta»c~ao a objetos. A prova, na sem^antica de rool, de que tais leis s~ao corretas, ¶e tamb¶em uma contribui»c~ao do presente trabalho. Apresentamos refactorings como regras alg¶ebricas de re¯namento envolvendo programas. A prova da preserva»c~ao do comportamento ¶e realizada pela aplica»c~ao de leis de programa»c~ao a um lado da regra a ¯m de obtermos o lado oposto. N¶os generalizamos a t¶ecnica padr~ao de re¯namento de dados a ¯m de lidar com hierarquia de classes. Neste trabalho tamb¶em apresentamos como obter um sistema estruturado segundo um padr~ao de projeto, por meio da aplica»c~ao de regras de refactoring. Padr~oes de projeto constituem-se num objetivo natural para a realiza»c~ao de transforma»c~oes por meio da aplica»c~ao de refactorings. Trabalhos presentes na literatura sobre padr~oes de projeto que prop~oem a formaliza»c~ao dos mesmos, em geral, concentram-se em suas descri»c~oes formais, n~ao na transforma»c~ao de um sistema com vistas a estrutur¶a-lo de acordo com padr~oes de projeto. Tamb¶em apresentamos a transforma»c~ao de uma aplica»c~ao monol¶³tica para uma aplica»c~ao estruturada segundo um padr~ao arquitetural.