• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 8
  • 2
  • Tagged with
  • 10
  • 6
  • 4
  • 4
  • 3
  • 3
  • 3
  • 3
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • 2
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
1

Conhece-te a ti mesmo / Conhece-te a ti mesmo

Mostoni, Mirella Amalia 09 November 2006 (has links)
Os objetos artísticos do Conhece-te a ti mesmo apresentam-se como oráculos, assumindo na poética e na relação estabelecida com o espectador as conexões de sentido pertencentes a esse termo e a essa condição. Na parte dissertativa é primeiro apresentada uma investigação sobre o processo criativo desses objetos, os métodos heurísticos utilizados, as influências recebidas e as afinidades com outros trabalhos artísticos. Num segundo momento estuda-se como a metáfora oracular e os procedimentos utilizados na elaboração dos trabalhos podem situar-se nas questões contemporâneas da recepção. Na terceira etapa da dissertação reflete-se sobre as semelhanças da poética proposta com o conceito de arte exposto por Nietzsche no texto O Nascimento da Tragédia, as influências dessa obra na gênese da poética e as conseqüências dessa escolha para a recepção e o processo de criação. / The artistic object of Know Thyself present themselves as oracles, assuming in the poetical and the relation estabilished with spectator connections of meaning pertaining to this term and this condition. In the dissertation part, first is presented an inquiry on creative process of these objects, the heuristic methods used, the received influences and the affinities with other artistic work. In a second moment, Formulate Thyself, is studied how the oracular metaphor and the procedures used in elaboration of these work may be take place in contemporaries questions about reception. In the third chapter is reflected on the similarities of the poetical proposal with the concept of art displayed by Nietzsche in Birth of Tragedy, the influences of this text on the genesis of poetical and the consequences of this choice for reception and process of creation.
2

Conhece-te a ti mesmo / Conhece-te a ti mesmo

Mirella Amalia Mostoni 09 November 2006 (has links)
Os objetos artísticos do Conhece-te a ti mesmo apresentam-se como oráculos, assumindo na poética e na relação estabelecida com o espectador as conexões de sentido pertencentes a esse termo e a essa condição. Na parte dissertativa é primeiro apresentada uma investigação sobre o processo criativo desses objetos, os métodos heurísticos utilizados, as influências recebidas e as afinidades com outros trabalhos artísticos. Num segundo momento estuda-se como a metáfora oracular e os procedimentos utilizados na elaboração dos trabalhos podem situar-se nas questões contemporâneas da recepção. Na terceira etapa da dissertação reflete-se sobre as semelhanças da poética proposta com o conceito de arte exposto por Nietzsche no texto O Nascimento da Tragédia, as influências dessa obra na gênese da poética e as conseqüências dessa escolha para a recepção e o processo de criação. / The artistic object of Know Thyself present themselves as oracles, assuming in the poetical and the relation estabilished with spectator connections of meaning pertaining to this term and this condition. In the dissertation part, first is presented an inquiry on creative process of these objects, the heuristic methods used, the received influences and the affinities with other artistic work. In a second moment, Formulate Thyself, is studied how the oracular metaphor and the procedures used in elaboration of these work may be take place in contemporaries questions about reception. In the third chapter is reflected on the similarities of the poetical proposal with the concept of art displayed by Nietzsche in Birth of Tragedy, the influences of this text on the genesis of poetical and the consequences of this choice for reception and process of creation.
3

Um senhorio originado pela Palavra do Senhor: estudo exegético do Salmo 110

Barros, Paulo Freitas 30 September 2014 (has links)
Made available in DSpace on 2016-04-29T14:27:26Z (GMT). No. of bitstreams: 1 Paulo Freitas Barros.pdf: 1152526 bytes, checksum: 1a9117462edd5bc7ccdf8811e53b486e (MD5) Previous issue date: 2014-09-30 / The objective of this master s thesis is an exegetical analysis in which will be described the theological dimensions of Psalm 110. Based on philological studies of ancient Hebrew a new translation of this Psalm is presented, as literal as possible. The study covers the historical and cultural context of the Psalm 110 as well as the theological thoughts related to the king and the Lord, God of Israel. Through the principle of canonical exegesis, the study includes the observance of parallels between biblical texts, which explain each other. Psalm 110 will also be researched within the texts of the New Testament, thereby demonstrating its importance for the reflection about Jesus Christ / O objetivo da presente dissertação de mestrado é analisar exegeticamente as dimensões teológicas do Salmo 110. A partir dos estudos filológicos do texto originalmente composto em hebraico, é apresentada uma nova tradução, a mais literal possível. No mais, o estudo abrange o contexto histórico-cultural do Salmo 110, bem como a sua reflexão teológica sobre o rei e o Senhor, Deus de Israel. Acolhendo o princípio da exegese canônica, o estudo aqui apresentado se baseia, sobretudo, na observância dos paralelismos na Bíblia Hebraica, imaginando-se que os textos bíblicos se expliquem de forma mútua. Finalmente, será pesquisado como os textos do Novo Testamento trabalham com a reflexão teológica presente no Salmo 110
4

On test oracles for Simulink-like models / Oráculos de teste para modelos Simulink-like

Nardi, Paulo Augusto 12 December 2013 (has links)
Embedded systems are present in many fields of application where failure may be critical. Such systems often possess characteristics that hampers the testing activity, as large amount of produced data and temporal requirements which must be specified and evaluated. There are tools that support the development of models for analysis and simulation still in the design stage. After being evaluated, a model may be used as basis to the implementation. In this case, it is important to ensure that the model is consistent with the specification. Otherwise, a divergence will be propagated to the final code. Therefore, the model must be tested prior to the codification. Simulink is a standard development and simulation tool for models of embedded systems. Its wide application in the industry has promoted the creation of free-software alternatives, as XCos. In the literature, there are researches which seek to improve the testing activity for Simulink-like models. The proposed solutions usually focus on test case selection strategies. However, little efforts have been directed to the oracle problem, that is, the difficulty in evaluating if an execution agrees with the specification. The objective of this doctorate proposal is to provide an oracle generation approach for Simulink-like models which addresses the characteristics previously summarized. Specifically, it is proposed a process, methods, procedures and a tool that enable the partially-automated generation of oracles for such models. As a main contribution, it is expected an improvement in the evaluation process of embedded systems in terms of quality, cost and time / Sistemas embarcados estão presentes em diversas áreas de aplicação em que falhas podem ser críticas. Tais sistemas frequentemente possuem características que tornam a fase de teste particularmente desafiadora, como a produção de grande quantidade de dados e requisitos temporais que precisam ser validados de acordo com a especificação. Existem ferramentas que auxiliam no desenvolvimento de modelos para análise e simulação do comportamento de sistemas embarcados ainda na fase de design. Após ser avaliado, o modelo pode ser usado como base para a implementação. Neste caso, deve-se buscar garantir que um modelo esteja de acordo com a especificação. Do contrário, tal divergência será propagada para a implementação. Portanto, e importante que o modelo seja testado antes da fase de implementação. Simulink e uma ferramenta-padrão de desenvolvimento e simulação de modelos de sistemas embarcados. Sua ampla aplicação na indústria incentivou a criação de alternativas de software livres como XCos. Na literatura, existem pesquisas que visam a aprimorar a atividade de teste de modelos Simulink-like. As soluções propostas geralmente focam em estratégias de seleção de casos de teste. Mas pouco esforço tem sido direcionado ao problema do oráculo, isto e, na dificuldade em avaliar se a execução está de acordo com a especificação. O objetivo desta proposta de doutorado é prover uma abordagem de geração de oráculos de teste para modelos simulink-like que contemple as características previamente resumidas. Especificamente, é proposto um processo, métodos, procedimentos e uma ferramenta que viabilizem a geração parcialmente automatizada de oráculos de teste para modelos Simulink-like. Como contribuição principal, é esperada a melhora da qualidade, custo e tempo do processo de validação de sistemas embarcados suportados por modelagem em Simulink e ferramentas similares
5

NÃO TEMAS! GRITEI POR TEU NOME: Estudo da concepção materna de Javé em Dêutero- Isaías a partir da análise exegética de Is 43,1-7 / Fear Not! Shouted for thy name: Study conception maternal Yahweh in Second Isaiah from the exegetical analysis of Is 43,1-7

Matos, Sue Hellen Monteiro de 26 August 2013 (has links)
Made available in DSpace on 2016-08-03T12:19:31Z (GMT). No. of bitstreams: 1 SUEHELLEN MONTEIRO DE MATOS.pdf: 677634 bytes, checksum: 59a28d5b0f6afe29b7c40c031f6365be (MD5) Previous issue date: 2013-08-26 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This exegetical study aims to demonstrate the maternal face of Yahweh revealed in the writings of Deutero-Isaiah, having as main source the oracle of salvation Is 43.1-7. To this end, we start from the analysis of the literary context, historical and religious Deutero-Isaiah, so that make the exegetical analysis of the text proposed by which we will focus, among various contents, the characteristic maternal presented in the passage. Understanding a text arises within a social environment, will highlight, based on the writings Deutero-Isaiah, the exiled community to which they are addressed prophets and prophetesses. Finally, combining the attributes of maternal goddesses Asherah and Ishtar with the fledgling maternal conception of Yahweh made by Hosea, we propose the maternal face of God based on texts of Deutero-Isaiah, in particular Is 43.1 to 7. / O presente estudo exegético tem por objetivo demonstrar a face materna de Javé revelada nos textos de Dêutero-Isaías, tendo como fonte principal o oráculo de salvação de Is 43,1-7. Para tal, partimos da análise do contexto literário, histórico e religioso de Dêutero-Isaías, paraentão fazer a análise exegética do texto proposto, através da qual enfocaremos, dentre os diversos conteúdos, a característica materna apresentada na perícope. Compreendendo que um texto surge dentro de um ambiente social, evidenciaremos, com base nos escritos de Dêutero-Isaías, a comunidade exilada à qual se dirigem profetas e profetisas. Por fim, combinando os atributos maternos das deusas Asherah e Ishtar com a incipiente concepção materna de Javé apresentado por Oséias, propomos a face materna de Deus com base nos textos dêuteroisaiânicos, em especial, Is 43,1-7.
6

Identidade e território como norte do processo de criação teatral de rua: buraco d'Oráculo e pombas urbanas nos limites da zona leste de São Paulo

Teixeira, Adailtom Alves [UNESP] 30 March 2012 (has links) (PDF)
Made available in DSpace on 2014-06-11T19:22:27Z (GMT). No. of bitstreams: 0 Previous issue date: 2012-03-30Bitstream added on 2014-06-13T20:49:01Z : No. of bitstreams: 1 teixeira_aa_me_ia.pdf: 1250340 bytes, checksum: 8bfbbb814f41688f96f5d7205dfbdfc8 (MD5) / Universidade Estadual Paulista (UNESP) / A pesquisa tem por objetivo analisar alguns espetáculos criados para a rua, buscando identificar de que maneira a identidade (sentimento de pertencimento) e o território (o espaço significado) influenciam nesse processo. Os dois grupos pesquisados, Pombas Urbanas e Buraco d`Oráculo, estão sediados na parte leste da cidade de São Paulo (SP), local basicamente habitado por trabalhadores migrantes ou por seus descendentes. Uma característica comum é que ambos os grupos criam seus espetáculos com base na observação da realidade na qual estão inseridos. Trataremos de quatro espetáculos: Mingau de concreto e Histórias para serem contadas (Pombas Urbanas); O cuscuz fedegoso e Ser TÃO Ser – narrativas da outra margem (Buraco d`Oráculo), de forma a tornar clara a relação aludida / La investigación tiene como objetivo examinar algunas creaciones producidas para la calle, de modo a identificar de que manera la identidad (sentido de pertenencia) y el territorio (espacio sentido) influyen en este proceso. Los dos grupos, Pombas Urbanas y Buraco d`Oráculo, se encuentran en la porción oriental de la ciudad de São Paulo (SP), el lugar habitado principalmente por trabajadores migratorios o sus descendiente. Una característica común a ambos grupos es la creación de sus espectáculos a partir de la observación de la realidad a la que pertenecen. Trataremos de cuatro espectáculos: Mingau de concreto y Histórias para serem contadas (Pombas Urbanas); O cuscuz fedegoso e Ser TÃO Ser – narrativas da outra margem (Buraco d`Oráculo), con el fín de aclarar la relación que ya hemos aludido
7

On test oracles for Simulink-like models / Oráculos de teste para modelos Simulink-like

Paulo Augusto Nardi 12 December 2013 (has links)
Embedded systems are present in many fields of application where failure may be critical. Such systems often possess characteristics that hampers the testing activity, as large amount of produced data and temporal requirements which must be specified and evaluated. There are tools that support the development of models for analysis and simulation still in the design stage. After being evaluated, a model may be used as basis to the implementation. In this case, it is important to ensure that the model is consistent with the specification. Otherwise, a divergence will be propagated to the final code. Therefore, the model must be tested prior to the codification. Simulink is a standard development and simulation tool for models of embedded systems. Its wide application in the industry has promoted the creation of free-software alternatives, as XCos. In the literature, there are researches which seek to improve the testing activity for Simulink-like models. The proposed solutions usually focus on test case selection strategies. However, little efforts have been directed to the oracle problem, that is, the difficulty in evaluating if an execution agrees with the specification. The objective of this doctorate proposal is to provide an oracle generation approach for Simulink-like models which addresses the characteristics previously summarized. Specifically, it is proposed a process, methods, procedures and a tool that enable the partially-automated generation of oracles for such models. As a main contribution, it is expected an improvement in the evaluation process of embedded systems in terms of quality, cost and time / Sistemas embarcados estão presentes em diversas áreas de aplicação em que falhas podem ser críticas. Tais sistemas frequentemente possuem características que tornam a fase de teste particularmente desafiadora, como a produção de grande quantidade de dados e requisitos temporais que precisam ser validados de acordo com a especificação. Existem ferramentas que auxiliam no desenvolvimento de modelos para análise e simulação do comportamento de sistemas embarcados ainda na fase de design. Após ser avaliado, o modelo pode ser usado como base para a implementação. Neste caso, deve-se buscar garantir que um modelo esteja de acordo com a especificação. Do contrário, tal divergência será propagada para a implementação. Portanto, e importante que o modelo seja testado antes da fase de implementação. Simulink e uma ferramenta-padrão de desenvolvimento e simulação de modelos de sistemas embarcados. Sua ampla aplicação na indústria incentivou a criação de alternativas de software livres como XCos. Na literatura, existem pesquisas que visam a aprimorar a atividade de teste de modelos Simulink-like. As soluções propostas geralmente focam em estratégias de seleção de casos de teste. Mas pouco esforço tem sido direcionado ao problema do oráculo, isto e, na dificuldade em avaliar se a execução está de acordo com a especificação. O objetivo desta proposta de doutorado é prover uma abordagem de geração de oráculos de teste para modelos simulink-like que contemple as características previamente resumidas. Especificamente, é proposto um processo, métodos, procedimentos e uma ferramenta que viabilizem a geração parcialmente automatizada de oráculos de teste para modelos Simulink-like. Como contribuição principal, é esperada a melhora da qualidade, custo e tempo do processo de validação de sistemas embarcados suportados por modelagem em Simulink e ferramentas similares
8

Perspectivas hermenêuticas de Isaías 45,1-7: Uma análise do título messiânico atribuído a Ciro. / Hermeneutic perspectives of Isaiah 45,1-7: An analysis of the messianic heading attributed the Cyrus

Silva, Roberto de Jesus 07 March 2013 (has links)
Made available in DSpace on 2016-08-03T12:19:23Z (GMT). No. of bitstreams: 1 Roberto de Jesus.pdf: 990691 bytes, checksum: 45c590bc6782917477256fbccbf6764a (MD5) Previous issue date: 2013-03-07 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The book of the prophet Dêutero-Isaiah approaches that Javé comes to console its people exiled in Babylonia. Foreign king Cyrus, in the text of Is 45,1-7 is intitled of Messiahs de Javé. Therefore, this research has as objective to reflect on the messianic heading attribution to king Cyrus, in the context of the Babylonian exile. For this, I analyze some contributions of diverse authors and authors of the Biblical area, exploring the diversity of analyses on this subject. It has many interpretations on the meaning of the messianic heading attributed to the king Cyrus, between them, it has who defines Cyrus as the Messiahs de Javé, that is, Cyrus as liberating of the exiled ones and not as the substitute of the messianic hope in a Messiahs proceeding from the house of David. In this work, I still argue has messianic hope, manifest in the exilic period and after-exilic, detaching the faith that the messianic communities exerted in these periods. At last, I analyze the messianic of the neo-testamentary communities after-macabaicas and in the attempt discovering if Cyrus was one messianic figure, in these periods. / O livro do profeta Dêutero-Isaías aborda que Javé vem consolar seu povo exilado na Babilônia. O rei estrangeiro Ciro, no texto de Is 45,1-7 é intitulado de Messias de Javé. Portanto, esta pesquisa tem como objetivo refletir sobre o título messiânico atribuído ao rei Ciro, no contexto do exílio babilônico. Para isto, analiso algumas contribuições de diversos autores e autoras da área bíblica, explorando a diversidade de pesquisas sobre este tema. Há muitas interpretações sobre o significado do título messiânico atribuído ao rei Ciro, entre elas, há quem define Ciro como o Messias de Javé, ou seja, Ciro como libertador dos exilados e não como o substituto da esperança messiânica em um Messias proveniente da casa de Davi. Neste trabalho, discuto ainda a esperança messiânica, manifesta no período exílico e pós-exílico, destacando a fé que as comunidades messiânicas exerciam nestes períodos. Enfim, analiso o messianismo das comunidades pós-macabaicas e neo-testamentárias na tentativa de descobrir se Ciro era uma figura messiânica, nestes períodos.
9

O caráter oracular da mídia

Moreira, Nádia Maria Lebedev Martinez 11 December 2015 (has links)
Made available in DSpace on 2016-04-26T18:15:25Z (GMT). No. of bitstreams: 1 Nadia Maria Lebedev Martinez Moreira.pdf: 4678006 bytes, checksum: 73d01e7fc9a37307118ccc3bbf867acb (MD5) Previous issue date: 2015-12-11 / Conselho Nacional de Desenvolvimento Científico e Tecnológico / The research aim to establish a direct relationship between its subjects, the Oracle and the Media. The main hypothesis is that the media has an oracular character. This reflection seems to be new within the Media Theory studies, and speculates that the future has a present event status. The oracles, or oracular character figures, when performing their predictions, design the future in the present, building scenarios that guide both the individual in his private life, as the society as a whole. The adopted methodological strategy sought to develop an archeology of the oracles in the West - especially the Oracle of Delphi, given its importance to the emergence of Western civilization and its institutions, including the media itself understanding them as backers of information, also a defining characteristic of the media. Researches concepts proposed by the Theory of Media in the reflections of Norval Baitello, Harry Pross and Flusser. Anxiety about the future is read from Soren Kierkegaard and Carl Gustav Jung. Within the concept of cultural anxiety Rafael Lopez-Pedraza, thinks the relationship of individuals and society in the future, this relationship also studied by Julian Jaynes in his deconstruction of the bicameral mind. Also Norbert Elias, who investigates what he calls a society of individuals. The hypothesis is tested trough media examples that analyze topics such as the economic crisis brought by the US housing bubble; Brazilian water crisis in 2015; and predictions about games results in sporting championships / A pesquisa procurou estabelecer uma relação direta entre seus objetos de estudo, o Oráculo e a Mídia. A hipótese principal é que a mídia possui um caráter oracular. Essa reflexão parece ser nova dentro dos estudos da Teoria da Mídia, e especula sobre o futuro como um estado de acontecimento presente. São os oráculos, ou de figuras de caráter oracular, que ao realizarem suas previsões, projetam o futuro no presente, construindo cenários que orientam tanto o indivíduo em sua vida particular, quanto à sociedade como um todo. A estratégia metodológica adotada buscou elaborar uma arqueologia dos oráculos no Ocidente principalmente do Oráculo de Delfos, dada sua importância fundante para o surgimento da civilização Ocidental e de suas instituições, entre elas, a própria mídia , entendendo-os como veiculadores de informações, característica também definidora do midiático. A pesquisa estuda conceitos propostos pela Teoria da Mídia nas reflexões de Norval Baitello, Harry Pross e Vilém Flusser. A angústia com relação ao futuro é lida a partir de Soren Kierkegaard e Carl Gustav Jung. Com o conceito ansiedade cultural de Rafael Lopez-Pedraza, pensa-se a relação dos indivíduos e da sociedade com o futuro, relação essa estudada também em Julian Jaynes com sua desconstrução da mente bicameral. Além de Norbert Elias, que investiga o que ele mesmo denomina de sociedade dos indivíduos. A hipótese é testada a partir de exemplos midiáticos que analisam temas como a crise econômica instaurada pela bolha imobiliária americana; a crise hídrica brasileira em 2015; e previsões feitas sobre resultados de jogos em campeonatos esportivos
10

Uma técnica para verificar não-conformidades em Programas Especificados com Contratos. / A technique for verifying nonconformities in Specified Programs with Contracts.

OLIVEIRA, Catuxe Varjão de Santana. 31 August 2018 (has links)
Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-31T22:55:43Z No. of bitstreams: 1 CATUXE VARJÃO DE SANTANA OLIVEIRA - PPGCC DISSERTAÇÃO 2013..pdf: 11354934 bytes, checksum: 6a23f31ef43ba211aeaa89eb36061a43 (MD5) / Made available in DSpace on 2018-08-31T22:55:43Z (GMT). No. of bitstreams: 1 CATUXE VARJÃO DE SANTANA OLIVEIRA - PPGCC DISSERTAÇÃO 2013..pdf: 11354934 bytes, checksum: 6a23f31ef43ba211aeaa89eb36061a43 (MD5) Previous issue date: 2013-03-15 / A escrita de especificações formais por contratos é uma maneira confiável e prática de construir softwares, em que desenvolvedores e clientes mantêm um acordo contendo direitos e obrigações a serem cumpridos. Essas responsabilidades são expressas basicamente através de pré-condições, pós-condições, e invariantes. Como exemplo de linguagem de especificação por contrato tem-se Java Modeling Language (JML) específica para programas Java. Apesar de a especificação formal melhorar a confiabilidade do software, deve-se haver certificação de que a implementação está em conformidade com a especificação definida. Verificação de conformidade em programas com contratos é geralmente realizada através de análises manuais ou verificação dinâmica, e em fases tardias do processo de desenvolvimento do software, ou seja, quando o produto final encontra-se disponível para o cliente. Nesta situação, o tempo despendido para detectar não-conformidades pode ser muito longo, ocasionando, consequentemente, atrasos no cronograma e aumento nos custos. Neste trabalho, propomos uma abordagem para checar conformidade entre código fonte e especificação formal por contratos através da geração e execução de testes. Testes de unidade são gerados automaticamente, resultando em casos de testes com sequências de chamadas aos métodos e construtores. Os contratos são transformados em assertivas que funcionam como oráculo para os testes. Esta abordagem não garante corretude total do software, mas aumenta a confiança quando uma não-conformidade é encontrada e, além disso, encoraja o uso de especificação por contratos. Nós implementamos JMLOK, uma ferramenta que executa os passos desta abordagem automaticamente no contexto de programas Java especificados com Java Modeling Language (JML). JMLOK foi avaliada em grupos de programas Java/JML, incluindo um módulo do projeto JavaCard. Todas as unidades experimentais totalizam 18 KLOC e 5K de linhas de especificação JML. Todo o processo consumiu menos que 10 minutos de execução e gerou como resultado a detecção de 29 não-conformidades. As causas das ocorrências das não-conformidades foram analisadas manualmente e classificadas em categorias de falhas. / Writing formal specifications by contracts is a practical and reliable way to build softwares in which developers and clients keep an agreement with rights and obligations to be fulfilled. These responsibilities are expressed basically by pre-conditions, post-conditions and invariants. As example of specification language by contract there is Java Modeling Language (JML) that is specific to Java programs. Although formal specification improves software rehabihty, it should exist certification of conformance with defined specification. Verify conformance between programs and contracts is usually performed by manual analysis or dynamic verification, and in late stages of software development process, that is, when the final product is available to client. In this situation, the time required to detect nonconformances could be so long, causing, consequently, schedule delays and increased costs. In this work, we propose an approach to check conformance between source code and contract formal specification through testing generation and execution. Unit tests are generated automatically resulting in test cases with call sequences of methods and constructors. The contracts are translated in assertions that work like test oracle. We have implemented JMLOK, a tool performs the approach steps automatically in the context of Java programs specified with Java Modeling Language (JML). JMLOK was evaluated in Java/JML programs groups, including a module of the JavaCard project. All the experimental units totalize 18 KLOC and 5K lines of JML specification. All process took less than 10 minutes of running and generated as result 29 nonconformances. The causes of nonconformances occurring were analyzed manually and classified in categories of fails.

Page generated in 0.0225 seconds