Corpo e aprendizagem em Boris Cyrulnik e em Merleau-Ponty

This research seeks to identify views of the body and learning the authors Boris Cyrulnik and Merleau - Ponty, thus tracing reflective for the educational field in several areas, with emphasis on physical education paths . We notice that the above authors present a wide collection of books, needing to develop this theoretical construct a limitation in their works. Therefore , on the theme of the body , were used mainly books The Sixth Sense , Boris Cyrulnik and Phenomenology of Perception , Merleau- Ponty , as both present in their organizational context a specific chapter on this subject . The phenomenological approach is included as path to be taken to devise this study because it is based on daily reflections that the human being perceives through his experiences with his peers and mainstream culture. The phenomenological reduction was carried out from the readings and interpretations of texts, writers and commentators, as well as approaching with life aspects of experience as a police officer and professor of ethics. The interpretation points to the understanding of body and learning that can be propagated within the Physical Education and as a way to understand and learn the constructs lived through sensitivity. The design of the body, feelings and affections of Boris Cyrulnik firm the empathetic bonds between human beings, bringing confidence to explore the world, learning through the new link with the other. This notion is close to the notion of expressive body Merleau Ponty, who holds intentions in their gestures (movements), entwining in time and space. Boris Cyrulnik and Merleau-Ponty expressed as the human being is enigmatic, lying embedded in a social and cultural world, so the experiences to traçarem existential trajetória and learning need in order to enaltercer freedom of expression as a mechanism that can be deployed in the appropriation of concepts and the criticality of the subject facing widespread theories (biological, social, anthropological , etc.) . From the reflections of the research is that recomneda Physical Education , as epistemological working area apprenticeships stemmed body movements should enable reflection on their practice, other do be done, but enabling the creation of different senses and meanings each body attitude

Visitabilidade-vivenciabilidade em assentamentos informais : um estudo da acessibilidade de percursos urbanos no Conjunto Santa Terezinha em Fortaleza-CE

This research approaches the issue of accessibility in informal settlements, seeking for the challenges and limits defined by informal urban settings, about the application of accessibility parameters. Take the empirical universe as the Conjunto Santa Terezinha, located in Fortaleza- Ce. Initially, the study presents a reflection about the housing issue in Brazil and the informal settlementes in view of the Right to the City. In this sense, the main references are, the works of Suzanne Pasternak (2008), Nabil Bonduki (1998) and Erminia Maricato (1996-97), among others. Follows with the discussion of the concepts and classifications of this type of settlement, making a content analysis of legislation and regulations relating to accessibility and proposed the discussion of the accessible route as the right strategy for the city. In another step, the methodology of 'walking together' created by Dischinger (2000) was applied in a passage previously chosen, which the researcher follows the disabled person during the journey through city making records like photos and video. The comments and perceptions are compared to the spatial analysis of urban morphology, made from the method of Del Rio (1990) and Panerai (2006), and the parameters of NBR 9050. Knowledge of the area is enriched by the methodology of the production of space made by Henri Lefebvre in his book 'The production of space' (1974) with these categories: space conceived, perceived and lived. Another key reference of this author it s the book 'The Right to the City' (991), which allowed in-depth reflections on the social function of town. In conclusion, the study finds that to guarantee a minimum access conditions in informal sittlements it´s necessary to know the specifics of their morphology, their relations and urban practices in view of the visitability- experiencebility, describing it as complementary concepts

Marias : biopolítica, vida nua e resiliência

Taking the narrative of life of three women (homeless), Maria José (residente of a psychiatric hospital) and Maria de La Luz Cervantes (fictional character of Gabriel Garcia Marquez, accidentally intern in a psychiatric hospital), the dissertation "Marias: Biopolitics, bare life and their stories" brings Giorgio Agamben's theories referring to Naked Life and Homo Sacer, Michel Foucault's with the biopolitics and resiliences written by Boris Cyrulnik. Its on these three women life stories that the dissertation develops a imaginary concentration camp to work their lives and bodies subjection to the external power, the biopolitic

Narrativas do Brasil nas memórias de Pedro Nava

This thesis is a translation of work of the Brazilian doctor, Pedro da Silva Nava (1903-1984), in particular, his memoirs and chronicles, articulated with the writings of medicine history, aiming to defend that the autobiographical narratives are sources of research capable of promoting discussions on the expansion of the present at the confluence of complex and unequal society in constant changing process as the Brazilian. The theoretical and methodological support circulates around studies, proposals and thesis by Boaventura Santos about empowering past, destabilizing subjectivity, sociology of absences, cosmopolitan reason and translation work. The empirical support drawn from the literature produced by Nava were analyzed with reference this reasoning and studies that have facilitated the flow of translation among others, the studies of Antonio Candido, Arrigucci Jr., Boris Cyrulnik, Beatriz Sarlo, Ecléa Bosi, Ítalo Calvino, José Willington Germano, José Maria Cançado, Lev Vygotsky, Marilena Chauí, Paul Ricöeur and Walter Benjamim, without neglecting what we consider indispensable to scientific research, the production of relevant knowledge and prudent, in view of a decent life. The initial inflections reflect the subject of the Memoirs and its education/training, to then place the Memoir subject in the literary context, scientific, historical and Brazilian poetic (1972-2010), bringing great interpreters and discussing the rationale used by the Narrator that we defend stand closer to the cosmopolitan, showing the formation of narratives whose presence insert itself beforehand to modernist verve, linked to the discursive array against the literature as domination space, disseminated in Brazil in the early twentieth century. So, it articulate with those in which the concerns adjust the construction of the social formation of Brazil as a national heritage through literary narrative that focuses on a historical principle that becomes the past empowering, allowing his rereading, whose converge to memory, the lifestyles, the plurality of language and Brazilian culture, formed by several people, converging into a design not of culture but multiculturalism in Brazil. The memory issue was addressed in the space-time of experiences of being that narrates, shaped by a destabilizing subjectivity that sought to order the testimony of a time, a history and society, retelling them by creative imagination, almost fictional, to make circulate his knowledge about Brazil attached to his medical knowledge, as well as other subjects in his living group and other groups with whom they maintained contact. Thus, he portrayed both tangible and intangible cultural assets of the country as a form of preservation, giving them meanings and sense. It approaches, therefore, from the perspective of sociology of absences, the expansion of the present and by the logic inherent in his narratives of self and Brazil

Diálogos da Alma: uma outra história da loucura

The tesis intends to awake a new way of looking at madness. It presents as reference the Psychiatric Hospital Doctor João Machado (Natal/RN) and histories of life and narratives of four intern residents. The research in an ethical horizon, intends to give back to the subjects the voices long silented behind the institutions walls by their families and society in general. As well as to open the interpretations of science to receive and to dialogue with other itineraries of thought that, if on one hand does not restitute the explanation of the Real, on the other hand expresses other forms to see the world. Dislocated of the bigger social environment, the people identified as insane, construct their histories endowed with autonomy and displacements in relation to the social rules and structures that characterize our society, as much as in relation to the logical principles of thought that assume an objective and rational reality. As well as a remnants bedspread configured in a complex and unfinished object, the break up of histories of life of the interns, interviews with medical on psychiatrists to the Doctor João Machado Hospital, documents of the institution and depositions of that house, were the raw material to construct, with this tesis, another chapter of the 'history of madness'. In elapsing of the work innumerable voices have been heard. Some that study the phenomenon of madness, others that live this 'state of the being' in the world. We opt to detaching the first of an open conception on the theme through intellectuals as: João da Costa Machado, Ulysses Pernambucano, Nise da Silveira and Boris Cyrulnik. They express ethics compromised to the humanity of the being

Alimento como metáfora, metáfora como alimento : a arte de nutrir uma educação complexa

Cette narrative fait le parcours d une recherche et de ses reflexions ici annoncé comme une odissée gastronomique et une géografie gourmante , dont les elements interpretatifs rendent possible concevoir qu une lecture de la métaphore et de la stéthique alimentaire puissent contribuer pour penser une éducation sensible, complexe, une education guidée par une experimentation esthétique de la condition humaine, qui provoque les sens, qui permettent évoquer et récuperer les connaissances et les savoirs pertinents, et qui confirme l indissociabilité du sujet dans ses plusieurs poles : nature et culture, émotion et raison. Comme contribution epistémologique, la dissertation, cherche étendre la compréhension d études qui abordent le Corp, l Aliment, la Métaphore, l Esthétique et l Éducation, en déclanchant des relations entre les espaces académicien et cotidien, en expérimentant d autres formes de sentir, penser et d être dans le monde. Poussée par une raison gourmande, et comme dans un rituel de préparation d aliment, j opte par les rélations transversales des savoirs ; je construis un dialogue entre les auteurs de domaine de connaissances multiples, comme la Filosophie, l Antropologie, l Étologie et l Éducation, en travaillant une reconstruction de concepts. Pour la tâche de cette odissée gastronomique, je découvre l approche entre un programme, comme méthode, et un livre de recettes culinaires hermétiques. J ai choisi de construir des estratégies métodologiques qui indiquent les chemins sur les quelles l imagination, la créativité et la réinvention, non seulement puissent mais doivent servir comme des épiceries qui emprègne d odeurs, de saveurs et de couleurs la connaissance, sans laisser de côté la rigueur, principe inégociable dans une science ouverte. J ai choisi, pour m accompagner dans cet étude, des sages, des scientistes et des poètes, entre eux je fais remarquer Michel Onfray, Boris Cyrulnik, Merleau-Ponty, Edgar Morin e Conceição Almeida. Avec eux, j ai déssiné des cartes, goûté des géographies, des terres, des ciels. J ai fréquenter des histoires et des personnages concrets et imaginaires; j ai convoqué des souvenirs acumulés pendant l enfance, avec ses trames, ses textures, ses saveurs, ses parfuns, ses couleurs, ses images, ses gestes, ses mots et ses silences, où le corp devient un médiateur d accès à la connaissance. Comme artifice complémentaire pour suivre la route, je parie sur le rapport fondamental entre le corp, l aliment, la métaphore, l esthétique et l Éducation, je m utilise du Cinéma, en cherchant d apprendre dans cet art, une éxistentialité humaine par le rapport entre la vie, l aliment et les personnages. Finalement, je reaffirme l importance de nourir des affections par une formation et une manière de penser capables de conecté des connaissances d univers dinstingués, et qui contribuent pour une conscience de la condition humaine et l apprentissage d une éducation de la vie et pour la vie

O cuidar de enfermagem e da família à pessoa idosa no domicílio: uma abordagem etnográfica

O envelhecimento é um processo multidimensional que envolve entre outros os aspectos físico-biológicos, sociais, econômicos e psicológicos. Ao avaliar essa fase da vida dentro de uma visão social e cultural, percebe-se que ser idoso ou não varia com as concepções culturais, sendo necessário investigar as variações que atuam no processo e rege o fenômeno sociocultural da realidade em que se está inserido. Com o aumento da população idosa mundial, esse processo tende a se intensificar. Estima-se que até em 2050 existam cerca de dois bilhões de pessoas com mais de 60 anos no mundo, e a maioria delas vivendo em países em desenvolvimento. No Brasil, acredita-se que existam, atualmente, cerca de 20 milhões de idosos. A normatização e legislação brasileira de amparo ao idoso em relação à saúde iniciaram-se a partir da Constituição Federal de 1988 e da Lei 8080 que regulamenta o Sistema Único de Saúde em 1990, em seus níveis de complexidade: atenção básica, média e alta complexidade. Para auxiliar nessa prestação dos serviços na atenção básica de saúde é importante observar as condições sociais, culturais, econômicas e de saúde dos idosos e seus familiares. Nesse sentido, a visita ao domicílio e a avaliação deste idoso em seu ambiente doméstico torna-se fundamental para acompanhar o cuidar prestado e o quanto esse processo irá interferir no sistema de saúde, na família e na qualidade de vida dos idosos. Neste contexto, o enfermeiro como integrante da Equipe de Saúde da Família, presta assistência à saúde do idoso no domicílio. Nesse sentido, o objetivo do estudo é analisar o cuidado de enfermagem e da família à pessoa idosa no domicílio com vistas à identificação das influências socioculturais. Trata-se de um estudo do tipo descritivo e de abordagem qualitativa, norteados por princípios teórico-metodológicos da etnografia com vistas ao estudo da influência dos aspectos culturais e sociais na assistência da família e do enfermeiro à idosos em domicílio. Foi realizado no município de Santana do Matos, RN, tendo como participantes, idosos, familiares e enfermeiros da equipe da ESF, definidos a partir da população do município e obtendo-se uma amostra intencional de 25 participantes: 6 enfermeiras, 10 idosos e 9 grupos familiares. Para a coleta de informações, utilizou-se observação, entrevista, diário de campo e grupo focal. Os resultados foram apresentados em forma de narrativa descritiva, na perspectiva dos conceitos de Boris Cyrulnik, com análise interpretativa cultural de Geertz, na busca dos significados e símbolos próprios da cultura da velhice de idosos e dos seus familiares, sobre cuidados que são realizados, tanto pela família, como pelos enfermeiros em domicílio. Observou-se que a família e o cuidador, dentro de sua realidade social e cultural, precisam ser mais compreendidos pela equipe de saúde para ser melhor orientados e capacitados na realização do cuidar de forma adequada. Por sua vez, os profissionais de saúde, em especial o enfermeiro, enfrentam dificuldades para realizar o cuidado ao idoso no domicílio como a grande demanda de atribuições na unidade de saúde como consultas e atendimentos; falta de transporte até os domicílios; extensão territorial do município e das áreas assistidas; número de pessoas atendidas por cada equipe; falta de compreensão dos profissionais de saúde quanto à importância da visita domiciliária na atenção básica. Entendem a necessidade de realizar ações de promoção em saúde, prevenção de agravos e de educação em saúde, além de reconhecerem a importância de uma melhor formação acadêmica para atuar nessa perspectiva e contribuírem para as mudanças necessárias na prática dos cuidados ao idoso em domicílio

Masculinidade a prova: um estudo de inspiração fenomenologico - hermeneutico sobre a infertilidade masculina

Culturally, childbearing is understood as a situation that subjects will experience at some point in their lives, especially people who are married or have a similar affectionate relationship. Thus, to realize the inability to meet such a fate seems to be a natural cultural trigger of suffering, frustration and feelings of inadequacy and helplessness. Specifically for men, infertility is closely related to loss of masculinity, virility. He fails in his role as a male. This study sought to understand the impact that infertility have on the existence of a man who receives such a diagnosis, both in self-image as in their marital, sexual and professional roles. This study sets up as a hermeneutic phenomenological research based on the ideas of the philosopher Martin Heidegger. Participants were seven heterosexual, married and infertile men. Two interviews were conducted. The analysis of the material included both the material of the narratives, as the affectation of the researcher when interacting with the participants and their narratives, through phenomenological-hermeneutic interpretation. The results corroborate the literature that states the difficulty of the men, immersed in a context that defines them as virile, powerful and invulnerable to worry about issues related to health and disease. The possibility of any condition that impairs the reproductive capacity exceeds the acceptable limits of daily life for these men, not being recognized as a model of masculinity present in the condition in which they recognize. This leads to questions about their masculinity, role in the marital relationship and their existence. Thus, to recognize themselves as infertile surpass a medical diagnosis and is associated with the construction of meaning for their existence from the approximation with the infertility condition, which helps in redirecting their choices, restoring the project to be self and allowing further recognition as men. In the marital relationship, doing what they can to ensure, theirs happiness. Through these actions, they remain playing the role of family provider, showing that they are able to protect their wives and taking in assisted reproduction or adoption of children viable alternatives to fulfill the desire to leave a legacy and give a child to their wives and to society. Another result observed, refers to the ontological condition of care that characterizes the human being. The ways in which men are treated socially demonstrates a type of care that focuses on the development of characteristics such as strength, virility and determination but does not allow them to cope with the suffering of emotionally difficult situations, such as the diagnosis of infertility. At the end, the study gives rise to reflections on the need to provide a 12 space for men and their expressions of suffering, as well as to recognize their ability to overcome the painful and difficult situations

Relação amorosa e tentativa de suicídio na adolescência : uma questão de (des)amor

Suicide rates have been rising all over the world. In Rio Grande do Norte state, a study carried out by Dutra (1999) investigated suicide rates among youngsters and found that in 1997 alone 244 cases of suicide attempt were registered. The author took an interest in studying this phenomenon among adolescents after reviewing Dutra s study and the technical literature on suicide. In addition to that, another topic caught her attention and raised new research questions: suicide attempts motivated by love, i.e., the end of a relationship, the fantasy of being abandoned by a partner. These have made the author to question how love manifested itself among adolescents and how it could become a reason for adolescents to give up their lives. Based on the data she analyzed and the research questions she developed, her research objective was to understand how adolescents who have attempted suicide because of love-related reasons have gone through this experience. The theoretical reference for the research was the Client-centered Therapy and more specifically, the construct self , according to Carl Rogers. The methodological strategy was inspired by the existential-phenomenological strategy. It used the narrative as a research instrument, inspired by the work of Walter Benjamim (1994) which was developed into a research strategy by Schmidt (1990). Four youngsters (three male and one female) have participated in this study. They have attempted suicide for love-related reasons during dolescence, when they were 12 to 18 years old. The interviews were recorded on cassette tapes, transcribed and literalized into narratives. The understanding of the narratives was based on the meanings that emerged from the youngsters speeches, as well as from the moments that touched the author. These moments highlighted the meaning of the experience of giving up life and the experience of love-based relationship as experienced by the youngsters. The study detected, among the adolescents who were interviewed, the existence of impulsiveness related to the suicide attempt. Also, the majority of the interviewees came from unstructured family backgrounds and had lost of one of their parents or had to face their parents divorce. The suicide was attempted by these youngsters through the ingestion of medicines. The research also revealed that the youngsters had regretted attempting suicide and felt guilty about it. With regards to their self-evaluation, the author observed that the youngsters had low self-esteem, negative perceptions about themselves and distorted views of themselves. These findings helped the author to reflect on the close relationship between the construct self and the suicide attempt. She also observed that a few factors, i.e., family context, education, social and cultural values, have influenced the way the youngsters perceived themselves . The results of this research confirm the idea that we have to understand the suicide attempt as a multi-determined phenomenon. This study contributed to the analysis and reflection on the factors that contribute to suicide attempts thus providing a foundation for the development of public health programs and policies to deal with this topic

Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

Projeto de Sistemas Integrados de Propósito Geral Baseados em Redes em Chip Expandindo as Funcionalidades dos Roteadores para Execução de Operações: A plataforma IPNoSys

It bet on the next generation of computers as architecture with multiple processors and/or multicore processors. In this sense there are challenges related to features interconnection, operating frequency, the area on chip, power dissipation, performance and programmability. The mechanism of interconnection and communication it was considered ideal for this type of architecture are the networks-on-chip, due its scalability, reusability and intrinsic parallelism. The networks-on-chip communication is accomplished by transmitting packets that carry data and instructions that represent requests and responses between the processing elements interconnected by the network. The transmission of packets is accomplished as in a pipeline between the routers in the network, from source to destination of the communication, even allowing simultaneous communications between pairs of different sources and destinations. From this fact, it is proposed to transform the entire infrastructure communication of network-on-chip, using the routing mechanisms, arbitration and storage, in a parallel processing system for high performance. In this proposal, the packages are formed by instructions and data that represent the applications, which are executed on routers as well as they are transmitted, using the pipeline and parallel communication transmissions. In contrast, traditional processors are not used, but only single cores that control the access to memory. An implementation of this idea is called IPNoSys (Integrated Processing NoC System), which has an own programming model and a routing algorithm that guarantees the execution of all instructions in the packets, preventing situations of deadlock, livelock and starvation. This architecture provides mechanisms for input and output, interruption and operating system support. As proof of concept was developed a programming environment and a simulator for this architecture in SystemC, which allows configuration of various parameters and to obtain several results to evaluate it

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures

Agraphs: definição, implementação e suas ferramentas

Programs manipulate information. However, information is abstract in nature and needs to be represented, usually by data structures, making it possible to be manipulated. This work presents the AGraphs, a representation and exchange format of the data that uses typed directed graphs with a simulation of hyperedges and hierarchical graphs. Associated to the AGraphs format there is a manipulation library with a simple programming interface, tailored to the language being represented. The AGraphs format in ad-hoc manner was used as representation format in tools developed at UFRN, and, to make it more usable in other tools, an accurate description and the development of support tools was necessary. These accurate description and tools have been developed and are described in this work. This work compares the AGraphs format with other representation and exchange formats (e.g ATerms, GDL, GraphML, GraX, GXL and XML). The main objective this comparison is to capture important characteristics and where the AGraphs concepts can still evolve

Computabilidade no espaço dos intervalos reais: um modelo BSS intervalar

A matemática intervalar é uma teoria matemática originada na década de 60 com o objetivo de responder questões de exatidão e eficiência que surgem na prática da computação científica e na resolução de problemas numéricos. As abordagens clássicas para teoria da computabilidade tratam com problemas discretos (por exemplo, sobre os números naturais, números inteiros, strings sobre um alfabeto finito, grafos, etc.). No entanto, campos da matemática pura e aplicada tratam com problemas envolvendo números reais e números complexos. Isto acontece, por exemplo, em análise numérica, sistemas dinâmicos, geometria computacional e teoria da otimização. Assim, uma abordagem computacional para problemas contínuos é desejável, ou ainda necessária, para tratar formalmente com computações analógicas e computações científicas em geral. Na literatura existem diferentes abordagens para a computabilidade nos números reais, mas, uma importante diferença entre estas abordagens está na maneira como é representado o número real. Existem basicamente duas linhas de estudo da computabilidade no contínuo. Na primeira delas uma aproximação da saída com precisão arbitrária é computada a partir de uma aproximação razoável da entrada [Bra95]. A outra linha de pesquisa para computabilidade real foi desenvolvida por Blum, Shub e Smale [BSS89]. Nesta aproximação, as chamadas máquinas BSS, um número real é visto como uma entidade acabada e as funções computáveis são geradas a partir de uma classe de funções básicas (numa maneira similar às funções parciais recursivas). Nesta dissertação estudaremos o modelo BSS, usado para se caracterizar uma teoria da computabilidade sobre os números reais e estenderemos este para se modelar a computabilidade no espaço dos intervalos reais. Assim, aqui veremos uma aproximação para computabilidade intervalar epistemologicamente diferente da estudada por Bedregal e Acióly [Bed96, BA97a, BA97b], na qual um intervalo real é visto como o limite de intervalos racionais, e a computabilidade de uma função intervalar real depende da computabilidade de uma função sobre os intervalos racionais

Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B