Spelling suggestions: "subject:"refinamentos"" "subject:"refinamientos""
1 |
Refactoring as formal refinementsLopes Cornélio, Márcio January 2004 (has links)
Made available in DSpace on 2014-06-12T15:52:59Z (GMT). No. of bitstreams: 2
arquivo4837_1.pdf: 1490840 bytes, checksum: 1e2239b5952d87633b8a93c565229e3e (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2004 / 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.
|
2 |
A Refinement Theory for AlloyGheyi, Rohit January 2007 (has links)
Made available in DSpace on 2014-06-12T15:53:55Z (GMT). No. of bitstreams: 2
arquivo6386_1.pdf: 3378493 bytes, checksum: 2ea65399678659e12b1393a14ebbb799 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2007 / Refatoramentos são geralmente propostos de maneira ad hoc, porque é difíıcil provar
formalmente que eles preservam comportamento. Na prática, desenvolvedores, mesmo
utilizando ferramentas de refatoramento, têm que usar compilação e testes para garantir
que os refatoramentos são corretos. Esse cenário não é desejado principalmente no
desenvolvimento de sistemas críticos.
No caso de refatoramento de modelos de objetos, boa parte das transformações se
baseia em argumentações informais. Um outro problema é que as noções de equivalência
para modelos de objetos são muito concretas, no sentido que elas assumem que os modelos
devem possuir operações, ou os mesmos nomes e estruturas. Isso não é adequado em
várias situações: durante refatoramento de modelos, quando usamos elementos do modelo
que são auxiliares, ou quando os modelos comparados possuem elementos distintos,
mas que são relacionados.
Neste trabalho, nosso objetivo é propor um conjunto de transformações que preservam
semântica para Alloy, que é uma linguagem formal de modelagem orientada a objetos.
Nós especificamos em PVS um conjunto de regras de boa formação e estendemos
a semântica para Alloy, e mostramos que as transformações propostas são corretas no
provador de teoremas de PVS. Mostramos também que este conjunto de transformações
´e relativamente completo no sentido que, com ele, podemos derivar um conjunto representativo
de transformações.
Além disso, propomos uma noção de refinamentos mais abstrata e flexível para modelos
de objetos, na qual nosso conjunto de transformações se baseia. Esta noção foi
especificada em PVS, onde provamos algumas propriedades da mesma. Além de provarmos
que ela é composicional, relacionamos a mesma com a noção de refinamento de dados
para Z. Estas transformações são úteis não só para derivarmos refatoramentos formalmente,
como também para otimizações. Além disso, mostramos que as transformações
podem ser utilizadas para derivar refatoramentos que introduzem formalmente padrões
de projeto em Alloy
|
3 |
Geração automática de casos de teste CSP orientada por propósitosde Carvalho Nogueira, Sidney January 2006 (has links)
Made available in DSpace on 2014-06-12T15:59:45Z (GMT). No. of bitstreams: 2
arquivo5536_1.pdf: 1197982 bytes, checksum: 344557c29e4105a048177410482f40ca (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2006 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / O processo de desenvolvimento de software está sujeito a inserção de erros diversos cuja presença
compromete a qualidade final dos produtos de software. Teste é uma atividade dinâmica
e bastante custosa dentro das várias empregadas pela Garantia da Qualidade de Software. O
objetivo de teste é demonstrar que um comportamento específico (cenário) de um sistema foi
bem (passou no teste) ou mal sucedido (falhou no teste), através de um veredicto.
Automação de testes visa tornar o processo mais ágil em atividades repetitivas e menos suscetível
a erros humanos. Existem várias abordagens de geração automática de teste, baseadas
na representação formal do comportamento do sistema, que empregam diferentes critérios de
seleção para os testes. Quando o objetivo do teste é focar na investigação de certas propriedades
ou comportamentos importantes do sistema a ser testado, podemos utilizar o critério de seleção
denominado propósito de teste (test purposes).
CSP (Communicating Sequential Processes) é uma notação formal bastante expressiva, uma
álgebra de processos útil para especificar comportamentos de sistemas concorrentes e distribuídos,
de hardware e software. Infelizmente, não existe na literatura abordagens para geração
de testes diretamente a partir de álgebras de processo como CSP. As abordagens existentes
utilizam a representação operacional (sistemas de transições rotuladas LTS) dos processos
CSP.
O objetivo deste trabalho é introduzir uma estratégia para geração automática de testes consistentes
(sound), elaborada inteiramente a partir da semântica denotacional de CSP (notação
de processos e modelos semânticos). É definida uma teoria de testes baseada na Teoria de Testes
de Tretmans. Um ponto comum entre estas teorias é que o conjunto de ações de entrada
e saída para especificações (alfabetos), implementações e testes são separados, de forma a definir
com precisão os veredictos para execução dos testes e a relação de conformidade entre
implementação e especificação. Adicionalmente, uma relação de conformidade denotada cspioco
é introduzida em termos de refinamentos de processos para determinar se o processo que
representa a implementação a ser testada está coerente com o comportamento do processo da
especificação. É apresentada, ainda, a estrutura e a utilização de uma ferramenta implementada
com o propósito de avaliar esta abordagem dentro do ambiente de teste de um projeto de pesquisa
que envolve uma cooperação entre o CIn-UFPE e a Motorola Industrial Limitada. Alguns
experimentos práticos foram realizados neste contexto
|
4 |
Abordagem para geração automática de código para framework de automação de testesARCOVERDE NETO, Euclides Napoleão January 2007 (has links)
Made available in DSpace on 2014-06-12T15:57:05Z (GMT). No. of bitstreams: 2
arquivo3138_1.pdf: 1790380 bytes, checksum: 8d08d6e97caeb1942c705627bab1ddc6 (MD5)
license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5)
Previous issue date: 2007 / Centro de Estudos Avançados do Recife / Engenharia de software visa criar software de maneira econômica, que seja confiável e que
trabalhe eficientemente em máquinas reais. Um de seus principais objetivos é obter um grau
de qualidade mínimo que, em geral, significa uma baixa taxa de defeitos. Considerando que
qualidade é crítico para o sucesso do software, o uso de testes vem crescendo. Testes objetivam
revelar a presença de erros o mais cedo possível no ciclo de desenvolvimento. Embora teste de
software seja uma atividade complexa, geralmente não é realizada sistematicamente devido a
uma série de fatores como limitações de tempo, recursos e qualificação técnica dos envolvidos.
Dessa forma, a automação de testes é uma tendência na área de testes.
Esse trabalho está inserido no contexto de um projeto de pesquisa realizado pela Motorola
em parceria com o Centro de Informática da Universidade Federal de Pernambuco denominado
CInBTCRD (CIn and Brazil Test Center Research and Development Project). Na Motorola, a
automação de testes faz-se por meio de um framework denominado de TAF (Test Automation
Framework), o qual simula a interação de um ser humano com um aparelho celular, além de
poder capturar o estado e outras informações importantes do aparelho.
Testes reusam implementações já definidas no TAF para criar os scripts de teste, bem como
novas implementações são criadas quando o reuso não é possível. Visto que bastante tempo é
gasto para criar tais implementações, este trabalho propõe criar uma estratégia que, dado um
script de teste, gere código para o TAF das funcionalidades ainda não implementadas automaticamente.
Para gerar tais códigos, foi utilizada a linguagem formal CSP (Communicating Sequential
Processes) como base. CSP foi criada para especificar e projetar comportamentos de sistemas
concorrentes e distribuídos. CSP possui uma teoria de refinamentos associada, a qual é o alicerce
de nossa proposta. O uso de refinamento em nossa proposta é relativamente simples:
dado um teste em TAF descrito usando CSP e o comportamento de um celular também em
CSP, a relação de refinamento só será satisfeita quando todos os elementos contidos no teste
estiverem de acordo com o definido no comportamento do celular. Assim sendo, nesse trabalho
usamos a ferramenta BxT (Behavior Extractor Tool) que desenvolvemos no contexto do projeto
de pesquisa para extrair automaticamente um modelo CSP de um celular, bem como reusamos
um outro trabalho que consegue representar casos de teste em CSP e criamos um algoritmo que
usa esses elementos e a teoria da refinamento de CSP para completar certas partes do caso de
teste com o auxílio do modelo do celular. Finalmente, o teste em CSP resultante é novamente
escrito em TAF e dessa forma conseguimos atualizar o framework automaticamente
|
5 |
Um ensaio em teoria dos jogos / An essay on game theoryPimentel, Edgard Almeida 16 August 2010 (has links)
Esta dissertação aborda a teoria dos jogos diferenciais em sua estreita relação com a teoria das equações de Hamilton-Jacobi (HJ). Inicialmente, uma revisão da noção de solução em teoria dos jogos é empreendida. Discutem-se nesta ocasião as idéias de equilíbrio de Nash e alguns de seus refinamentos. Em seguida, tem lugar uma introdução à teoria dos jogos diferenciais, onde noções de solução como a função de valor de Isaacs e de Friedman são discutidas. É nesta altura do trabalho que fica evidente a conexão entre este conceito de solução e a teoria das equações de Hamilton-Jacobi. Por ocasião desta conexão, é explorada a noção de solução clássica e é exposta uma demonstração do fato de que se um jogo diferencial possuir uma função de valor pelo menos continuamente diferenciável, esta será uma solução da equação de Hamilton-Jacobi associada ao jogo. Este resultado faz uso do princípio da programação dinâmica, devido a Bellman, e cuja demonstração está presente no texto. No entanto, quando a função de valor do jogo é apenas contínua, então embora esta não seja uma solução clássica da equação HJ associada a jogo, vemos que ela será uma solução viscosa, ou solução no sentido da viscosidade - e a esta altura são discutidos os elementos e propriedades desta classe de soluções, um teorema de existência e unicidade e alguns exemplos. Por fim, retomamos o estudo dos jogos diferenciais à luz das soluções viscosas da equação de Hamilton-Jacobi e, assim, expomos uma demonstração de existência da função de valor e do princípio da programação dinâmica a partir das noções da viscosidade / This dissertation aims to address the topic of Differential Game Theory in its connection with the Hamilton-Jacobi (HJ) equations framework. Firstly we introduce the idea of solution for a game, through the discussion of Nash equilibria and its refinements. Secondly, the solution concept is then translated to the context of Differential Games and the idea of value function is introduced in its Isaacs\'s as well as Friedman\'s version. As the value function is discussed, its relationship with the Hamilton-Jacobi equations theory becomes self-evident. Due to such relation, we investigate the HJ equation from two distinct points of view. First of all, we discuss a statement according to which if a differential game has a continuously differentiable value function, then such function is a classical solution of the HJ equation associated to the game. This result strongly relies on Bellman\'s Dynamic Programming Principle - and this is the reason why we devote an entire chapter to this theme. Furthermore, HJ is still at our sight from the PDE point of view. Our motivation is simple: under some lack of regularity - a value function which is continuous, but not continuously differentiable - a game may still have a value function represented as a solution of the associated HJ equation. In this case such a solution will be called a solution in the viscosity sense. We then discuss the properties of viscosity solutions as well as provide an existence and uniqueness theorem. Finally we turn our attention back to the theory of games and - through the notion of viscosity - establish the existence and uniqueness of value functions for a differential game within viscosity solution theory.
|
6 |
Um ensaio em teoria dos jogos / An essay on game theoryEdgard Almeida Pimentel 16 August 2010 (has links)
Esta dissertação aborda a teoria dos jogos diferenciais em sua estreita relação com a teoria das equações de Hamilton-Jacobi (HJ). Inicialmente, uma revisão da noção de solução em teoria dos jogos é empreendida. Discutem-se nesta ocasião as idéias de equilíbrio de Nash e alguns de seus refinamentos. Em seguida, tem lugar uma introdução à teoria dos jogos diferenciais, onde noções de solução como a função de valor de Isaacs e de Friedman são discutidas. É nesta altura do trabalho que fica evidente a conexão entre este conceito de solução e a teoria das equações de Hamilton-Jacobi. Por ocasião desta conexão, é explorada a noção de solução clássica e é exposta uma demonstração do fato de que se um jogo diferencial possuir uma função de valor pelo menos continuamente diferenciável, esta será uma solução da equação de Hamilton-Jacobi associada ao jogo. Este resultado faz uso do princípio da programação dinâmica, devido a Bellman, e cuja demonstração está presente no texto. No entanto, quando a função de valor do jogo é apenas contínua, então embora esta não seja uma solução clássica da equação HJ associada a jogo, vemos que ela será uma solução viscosa, ou solução no sentido da viscosidade - e a esta altura são discutidos os elementos e propriedades desta classe de soluções, um teorema de existência e unicidade e alguns exemplos. Por fim, retomamos o estudo dos jogos diferenciais à luz das soluções viscosas da equação de Hamilton-Jacobi e, assim, expomos uma demonstração de existência da função de valor e do princípio da programação dinâmica a partir das noções da viscosidade / This dissertation aims to address the topic of Differential Game Theory in its connection with the Hamilton-Jacobi (HJ) equations framework. Firstly we introduce the idea of solution for a game, through the discussion of Nash equilibria and its refinements. Secondly, the solution concept is then translated to the context of Differential Games and the idea of value function is introduced in its Isaacs\'s as well as Friedman\'s version. As the value function is discussed, its relationship with the Hamilton-Jacobi equations theory becomes self-evident. Due to such relation, we investigate the HJ equation from two distinct points of view. First of all, we discuss a statement according to which if a differential game has a continuously differentiable value function, then such function is a classical solution of the HJ equation associated to the game. This result strongly relies on Bellman\'s Dynamic Programming Principle - and this is the reason why we devote an entire chapter to this theme. Furthermore, HJ is still at our sight from the PDE point of view. Our motivation is simple: under some lack of regularity - a value function which is continuous, but not continuously differentiable - a game may still have a value function represented as a solution of the associated HJ equation. In this case such a solution will be called a solution in the viscosity sense. We then discuss the properties of viscosity solutions as well as provide an existence and uniqueness theorem. Finally we turn our attention back to the theory of games and - through the notion of viscosity - establish the existence and uniqueness of value functions for a differential game within viscosity solution theory.
|
Page generated in 0.0699 seconds