Interesses da habitação social : políticas e processos no Rio Grande do Norte

En 2003, le gouvernement brésilien (gestion Lula) a initié une nouvelle phase dans son histoire de l habitation, en intensifiant les constructions de logements sociaux au Brésil. Un tel accroissement a eut des répercussions tant en ville comme à la campagne, et fût marqué dans le Rio Grande do Norte, par la production a grande échelle d ensembles d habitations, dans les programmes de Gouvernement. Afin de viabiliser ces transformations, des instruments politiques, financiers et de gestion ont étés articulés conjointement, utilisant la répétition d une typologie d édification, comme modèle, accompagnée de la reproduction d une morphologie dans les constructions de logements sociaux. Afin de comprendre ce processus nous introduisons une recherche urbanistique et socio-économique du problème du logement social au Brésil, en cherchant à mettre en relation les aspects techniques avec les questions historique, professionnelles et culturelles, éléments complémentaires. Notre analyse cherche a identifier comment les politiques de gestion et financement officielles (administrées dans sa grande majorité par la Caisse Économique Fédérale -CEF-), influencent le processus de conception de projets, en provoquant les répétitions de type/morphologiques, déjà citées. Basée sur l observation directe au cour de deux expériences différenciées pour du logement social en milieu rural, au Rio Grande do Norte, nous montrerons aussi certaines limitations et possibilités des acteurs sociaux, face aux agents et politiques officielles pour le logement social au Brésil, proposant des solutions alternatives standardisées qui caractérisent le résultat des projets financées et gérés par la CEF. Nos principales références théoriques et méthodologiques sont Nabil Bonduki (1998), David Harvey (2009,1982), Henry Lefèbvre (1970), Ermínia Maricato (2010, 2009, 2000, 1987) et Raquel Rolnik (2010, 2009, 2008, 1997)

Os dias são maus : o ensino religioso cristão em dias pós-modernos o desafio de fazer crer perante a cultura da incredulidade

This paper adopts the assumption that religion continues to be a major highlight in the dimension of the contemporary world - characterized by pluralism, the ideas of tolerance and freedom. But for certain streams of Christianity, the postmodern culture seems to be characterized as a highly damaging to their doctrines and principles, since this religious matrix carries a truth claim that would support all its significance, its definition values and their dissemination effort ( evangelism ). This is not to say that Christianity is the only religion that claims to the truth, which would be a gross mistake. Now, religion has been reputed as a phenomenon doomed to disappear, according to the " ideology " of Modernity, given the idea that scientific development would lead us inevitably to the statement that religion was merely a social institution based in the superstition, in fantasy, the imaginary and therefore had nothing "real " unless its existence as an institution capable of aggregating society (give it cohesion), provide values and meaning to different ontological anxieties and doubts of humankind. In the contemporary scenario - seeded by modernity - as Christian ideas, doctrines and principles are in harmony or conflict with postmodernity? These are our starting questions and issues that we intend to stop and reflect. From the assumption that the religious phenomenon has great force in the present day, this research aims to perform central analysis of how religious education, a Protestant denomination specific, harmonizes or clashes with the ideology or ideas more general and emphatic that we can observe in the western world is presented to us from the diagnoses made by the contemporary authors who debate about postmodernism and postmodernity, notably David Harvey, Jean - François Lyotard, Bauman Zygmunt and Fredric Jameson

Um sonho distante: reflexões sobre acessibilidade nos conjuntos habitacionais do pmcmv faixa 1 na região metropolitana de Natal

This dissertation seeks to reflect on the accessibility of the governmental program Minha Casa Minha Vida, track 1, which comprehends people who made 0 to 3 minimum wages within the metropolitan region of Natal RN between the years of 2009 and 2012. The research covers the municipalities benefited by the program: Ceará-Mirim, Extremoz, Macaíba, Monte Alegre, Natal, Nísia Floresta, Parnamirim and São Gonçalo do Amarante. We have investigated the extensions of PMCMV on the context of the access to the city, debating some concepts attached to the capitalist mode of production such as residential segregation and peripherization. We have aimed to identify the accessibility conditions in the new housing complexes from three primal categories, namely, the localization of the complexes, the disponibility of public equipments, services, leisure and cultural properties on the neighborhood and the offer of public transport. Our theorical references are based on the ideas of the british geographer David Harvey on his work Social Justice and the City , from 1980. Harvey s studies made us debate on the locational choice for the social-matter habitation, and also let us discuss the price to accessibility on these new programs and its implications on the income of those who are benefited by them, specially because this is about a low-income population. To the achievement of these objectives, we made use of case study, including desk research, photographic documentation, records of field observations and informal conversations with locals, composing a qualitative study. In light of what has been researched and considering the guiding research questions, we reflect on aspects of the program that can greatly influence the processes of residential segregation and housing periphery of the lowincome population from the precarious conditions of accessibility to the referred population

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

Deciding difference logic in a Nelson-Oppen combination framework

O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria específica, possam ser combinados para inferir sobre teorias mais abrangentes, através do princípio de propagação de igualdades. Provadores de teorema baseados neste modelo são beneficiados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Difference logic é uma subteoria da aritmética linear. Ela é formada por constraints do tipo x − y ≤ c, onde x e y são variáveis e c é uma constante. Difference logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em vários outros casos. Difference logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que vários algoritmos eficientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decisão para difference logic é capaz de induzir sobre milhares de constraints. Um procedimento de decisão para a teoria de difference logic tem como objetivo principal informar se um conjunto de constraints de difference logic é satisfatível (as variáveis podem assumir valores que tornam o conjunto consistente) ou não. Além disso, para funcionar em um modelo de combinação baseado em Nelson-Oppen, o procedimento de decisão precisa ter outras funcionalidades, como geração de igualdade de variáveis, prova de inconsistência, premissas, etc. Este trabalho apresenta um procedimento de decisão para a teoria de difference logic dentro de uma arquitetura baseada no método de combinação de Nelson-Oppen. O trabalho foi realizado integrando-se ao provador haRVey, de onde foi possível observar o seu funcionamento. Detalhes de implementação e testes experimentais são relatados

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

Natal Condomínio Clube : inovação espacial nos eixos de valorização da zona sul da cidade

This dissertation is about new real estate development in the southward expansion area in Natal, Brazil, by use of high-rise condos, so-called club-condominiums. The area includes part of the neighboring municipality, Parnamirim, and focuses on the role played by urban developers in the housing market. The main feature in these condos are common areas filled with leisure equipments, allegedly to grant quality of life, comfort and tranquility to residents. The rapid development of the area takes advantage of large plots of land available as well as of urban infrastructure. Overall preference of middle-class sectors for the South area of Natal (and adjoining part of Parnamirim) is also a factor worth of note. For this reason, this part of the city constitutes one of the preferred areas of urban developers. This dissertation includes a discussion of Henri Lefebvre s production of space, emphasizing its tridimensional features. It draws on David Harvey s works to deal with transformations of the built environment regarding the dynamics of real estate markets; in particular, it considers the idea of creative destruction. Finally, the dissertation discusses the concepts developed by Pedro Abramo regarding the forms of operation by urban entrepreneurs, in particular the concepts of urban convention and spatial innovation. For the empirical work, a number of interviews with key entrepreneurs and civil servants were undertaken. In more general terms, it is worth observing that there is a direct relationship between the location of such developments and the process of spatial fragmentation, seen both as a consequence and a strategy of the way urban developers operate