Alternância no uso dos modos indicativo e subjuntivo em orações subordinadas substantivas: uma comparação entre o português do Brasil e o francês do Canadá

The purpose of this work is to analyze the use of the indicative mood, instead of the subjunctive prescribed by the normative grammar, in complement clauses introduced by the conjunction que in Brazilian Portuguese. Contexts of use of the subjunctive according to grammatical prescription, and contexts of fluctuation on the use of that verbal mood were analyzed, in an attempt to investigate what interferes on the choice of the mood by the user of the language. This study is based on North-American Functional Linguistics theoretical perspective, oriented to analyzing language in use, in the light of the principles of grammaticalization and markedness. The results obtained support that the contexts that favor the indicative over the subjunctive are those composed by a complement clause functioning as a direct object the unmarked clause of all complement clauses and by a verb on the main sentence that belongs to the semantic field of low certainty, corresponding to the epistemic sub-mode the unmarked category of the deontic sub-mode. The results indicate that pragmatics and semantics factors influence the language user on the choice of the verbal mood. This research also presents comparative data on the use of the indicative mood in place of the subjunctive in Brazilian Portuguese and Canadian French, aiming to providing suggestions on language teaching

A aplicações dos trataos internacionais de direitos humanos pela jurisdição brasileira

O Brasil, apesar de ter uma participação ativa nos fóruns internacionais de debates sobre a proteção dos direitos humanos, ainda não atua de forma eficiente no adimplemento das obrigações livremente pactuadas, fato este que o levou a ser acionado e condenado pela Corte Interamericana de Direitos Humanos, em virtude da prática de atos violatórios aos ditos direitos, praticados no âmbito dos três Poderes, bem como por todos os Entes Federativos. Diante dessa realidade que se apresenta, o nosso objeto de estudo será investigar a efetivação dos direitos humanos previstos em tratados internacionais pela Jurisdição brasileira. Na esteira desse raciocínio, nossa problemática consiste em demonstrar que os tratados internacionais de direitos humanos, apesar de serem claramente fontes do direito estatal, não vêm sendo devidamente aplicados pelos órgãos que exercem a função jurisdicional em nosso país. Fixada à problemática, nosso objetivo no presente estudo consiste em: 1) descrever a competência constitucional do Poder Judiciário para proteção dos direitos humanos e aplicação dos tratados internacionais; 2) definir o controle jurisdicional de convencionalidade como instrumento de proteção dos direitos humanos a ser utilizados pelos magistrados; e, 3) analisar quase um século de decisões do Supremo Tribunal Federal no que toca a aplicação dos tratados internacionais de direitos humanos. Espera-se efetivamente demonstrar que compete a todos os órgãos estatais o dever de aplicar diretamente os instrumentos internacionais de proteção aos direitos humanos devidamente internalizados. Essa obrigação inegavelmente também recai sobre os que exercem a função jurisdicional. Desta maneira, todos os juízes incumbidos do exercício da jurisdição convertem-se no âmbito estatal em verdadeiros concretizadores dos direitos humanos, sejam eles advindos do sistema global ou do regional de proteção. Dessa forma, devem servir-se do controle de convencionalidade para afastar as manifestações estatais que estejam em dissintonia com o teor dos tratados internacionais de direitos humanos, bem como da interpreção a eles conferida pelas Cortes e Tribunais internacionais

A ferramenta VoiceThread em uma abordagem hibrida: o desenvolvimento da produção oral e da habilidade de noticing na aprendizagem de inglês como L2

VoiceThread (VT) is a collaborative and asynchronous web 2.0 tool, which permits the creation of oral presentations with the help of images, documents, texts and voice, allowing groups of people to browse and contribute with comments using several options: voice (microphone or cell phone), text and audio-file or video (webcam) (BOTTENTUIT JUNIOR, LISBÔA E COUTINHO, 2009). The hybrid experience with VoiceThread allows learners to plan their speech before recording it, without the pressure often existent in the classroom. Furthermore, the presentations can be recorded several times, enabling students to listen to them, notice the gaps in their oral production (noticing) and edit innumerous times before publishing them online. In this perspective, oral production is seen as a process of L2 acquisition, not only as practice of already existent knowledge, because it can stimulate the learner to process the language syntactically (SWAIN, 1985; 1995). In this context, this study aims to verify if there is a relation between the oral production of the learners more specifically the grammatical accuracy and the global oral grade and their noticing capacity, how the systematic practice with VoiceThread, in a hybrid approach, can impact the learners global oral development, their oral production in terms of fluency (number of words per minute), accuracy (number of errors in hundred words), and complexity (number of dependent clauses per minute), and on their noticing capacity (SCHMIDT, 1990; 1995; 2001), that is, the learner s capacity of noticing the gaps existent in their oral production. In order to answer these research questions, 49 L2 learners of English were divided into an experimental group (25 students) and a control group (24 students). The experimental group was exposed to the hybrid approach with VT during two months and, through a pre- and post-test, we verified if this systematic practice would positively influence these participants oral production and noticing capacity. These results were compared to the pre- and post-test scores from the control group, which was not exposed to VT. Finally, learners impressions in relation to the use of this tool were also sought through a questionnaire applied after the post-test. The results indicate that there is a statistically significant correlation between the learners speech production (accuracy and global oral grade) and their noticing capacity. Besides, it was verified a positive impact of VoiceThread on the learners speech production variables and on their noticing capacity. They also reveal a positive reaction by the learners in relation to the hybrid experience with this web tool

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

Estendendo CRefine para o suporte de táticas de refinamento

The use of increasingly complex software applications is demanding greater investment in the development of such systems to ensure applications with better quality. Therefore, new techniques are being used in Software Engineering, thus making the development process more effective. Among these new approaches, we highlight Formal Methods, which use formal languages that are strongly based on mathematics and have a well-defined semantics and syntax. One of these languages is Circus, which can be used to model concurrent systems. It was developed from the union of concepts from two other specification languages: Z, which specifies systems with complex data, and CSP, which is normally used to model concurrent systems. Circus has an associated refinement calculus, which can be used to develop software in a precise and stepwise fashion. Each step is justified by the application of a refinement law (possibly with the discharge of proof obligations). Sometimes, the same laws can be applied in the same manner in different developments or even in different parts of a single development. A strategy to optimize this calculus is to formalise these application as a refinement tactic, which can then be used as a single transformation rule. CRefine was developed to support the Circus refinement calculus. However, before the work presented here, it did not provide support for refinement tactics. The aim of this work is to provide tool support for refinement tactics. For that, we develop a new module in CRefine, which automates the process of defining and applying refinement tactics that are formalised in the tactic language ArcAngelC. Finally, we validate the extension by applying the new module in a case study, which used the refinement tactics in a refinement strategy for verification of SPARK Ada implementations of control systems. In this work, we apply our module in the first two phases of this strategy

Formal verification of PLC programs using the B Method

PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs

Taxonomia de Papilionoideae (leguminosae) da Mata Atlântica do Rio Grande do Norte, Brasil

Leguminosae is the third largest family of angiosperms with about 19.325 species and 727 genera, and it is pantropically distributed. Papilionoideae is the most diverse of the three legume subfamilies, with around 13.800 species (71%), 478 genera, and 28 tribes. Papilionoid legumes include herbs, shrubs, lianas or trees with pinnate, trifoliolate, unifoliolate or simple leaves, flowers frequently papilionate with descending imbricate petal aestivation, the petals highly differentiated into standard, keel, and wings, androecium usually diplostemous, and seeds without pleurogram, with conspicuous hilum, and the embryo radicle usually curved. The current study aims to carry out a taxonomic account of the Papilionoideae from Atlantic Forest remnants in Rio Grande do Norte, Brazil, across the herbaria data surveys, collections of field samples and morphological analysis of the collected specimens and/or herbaria materials. Identification key, descriptions, diagnostic characters, illustrations, and geographic distribution of the 68 species and 32 genera within the following tribes Phaseoleae (11 genera/24 species), Dalbergieae (9/20), Swartzieae (3/3), Millettieae (2/4), Sophoreae (2/2), Abreae (1/1), Crotalarieae (1/3), Desmodieae (1/7), Indigofereae (1/3), and Sesbanieae (1/1). The most species-rich genera were Desmodium Desv. (7 species), Centrosema (DC.) Benth. (5), Stylosanthes Sw. (5), Aeschynomene L. (4) and Macroptilium (Benth.) Urb. (4). Concerning to the habit, the herbaceous and shrubby has predominated with 60% (41 spp.), following by the vine and lianas with 28% (19 spp.) and the woody with only 12% (8 spp.). Thirty two species and the following genera are newly recorded for the flora of Rio Grande do Norte: Chaetocalyx, Cochliasanthus, Crotalaria, Galactia, Geoffroea, Macroptilium, Rhynchosia, Swartzia, Trischidium, and Vigna

Limites e evolução geodinâmica do Sistema Jaguaribeano, Província Borborema, Nordeste do Brasil

The studied area is geologically located in the Northern Domain of the Borborema Province (Northeast Brazil), limited to the south by the Patos shear zone. Terranes of the Jaguaribeano system are dominant, flanked by the Piranhas (E and S sides) and Central Ceará (NE side) terranes. Its basement comprises gneiss -migmatite terrains of Paleoproterozoic to Archean age (2.6 to 1.9 Ga old), overprinted by neoproterozoic to cambrian tectonotherma l events. Narrow supracrustal belts ( schist belts) display a 1.6 to 1.8 Ga age, as shown by whole - rock Rb-Sr and zircon U-Pb and Pb/Pb dates in acid metavolcanics which dominate in the lower section of these sequences, and in coeval metaplutonics (granitic augen gneisses). From the stratigraphic point of view, three Staterian belts are recognized: 1. Orós Belt - made up by the Orós Group, subdivided in the Santarém (predominantly pure to impure quartzites, micaschists and metacarbonates) and Campo Alegre (metandesites, metabasalts, metarhyolites and metarhyodacites, interlayered with metatuffs and metasediments) formations, and by the Serra do Deserto Magmatic Suite (granitic augen gneisses). 2. Jaguaribe Belt - its lithostratigrahic-lithodemic framework is similar to the one of the Orós Belt, however with a greater expression of the volcano -plutonic components (Campo Alegre Formation and Serra do Deserto Magmatic Suite). The Peixe Gordo Sequence, separately described, is also related to this belt and contain s metasedimentary, metavolcanic (with subordinated volcanoclastics) and metaplutonic units. The first one correlated to the Orós Group and the latter the Serra do Deserto Magmatic Suite. 3. Western Potiguar Belt - represented by the Serra de São José Gro up, subdivided in the Catolezinho (biotite -amphibole gneisses with intercalations of metacarbonates, calcsilicate rocks, amphibolites and quartzite beds to the top) and Minhuins (quartzites, micaschists, metaconglomerates, calcsilicate rocks, acid to the b asic metavolcanics and metatuffs) formations. Its late Paleoproterozoic (Staterian) age was established by a Pb/Pb date on zircons from a granitic orthogneiss of the Catolezinho Formation. The petrographic characteristics and sedimentary structures of the Santarém Formation of the Orós Group point to deltaic to shallow marine depositional systems, overlain by deep water deposits (turbidites). The geodynamic setting of this region encompassed a large depositional basin, probably extending to the east of the Portalegre shear zone and west of the Senador Pompeu shear zone, with possible equivalents in the Jucurutu Formation of the Seridó Belt and in the Ceará Group of central Ceará. The Arneiróz Belt, west Ceará, displays some stratigraphic features and granito ids geochemically akin to the ones of the Orós Belt. The evolutionary setting started with an extensional phase which was more active in the eastern part of this domain (Western Potiguar and part of the Jaguaribe belts), where the rudite and psamite sedime ntation relates to a fluviatile rift environment which evolved to a prograding deltaic system to the west (Orós Group). The basaltic andesitic and rhyolitic volcanics were associated to this extensional phase. During this magmatic event, acid magmas also crystallized at plutonic depths. The Orós Group illustrates the environmental conditions in the western part of this domain. Later on, after a large time gap (1.6 to 1.1 Ga), the region was subjected to an extensional deformational episode marked by 900 Ma old (Sm-Nd data) basic rocks, possibly in connection with the deposition of the Cachoeirinha Group south of the Patos shear zone. In the 800 to 500 Ma age interval, the region was affected by important deformational and metamorphic events coupled with in trusion of granitic rocks of variable size (dykes to batholiths), related to the Brasiliano/Pan -African geotectonic cycle. These events produced structural blocks which differentiate, one from the other, according to the importance of anatectic mobilizatio n, proportion of high-grade supracrustals and the amount of neoproterozoic -cambrian granitoid intrusions. On this basis, a large portion of the Jaguaretama Block/Terrane is relatively well preserved from this late overprint. The border belts of the Jagua retama Block (Western Potiguar and Arneiroz) display kyanite-bearing (medium pressure) mineral associations, while in the inner part of the block there is a north-south metamorphic zoning marked by staurolite or sillimanite peak metamorphic conditions. Regarding the deformations of the Staterian supracrustal rocks, second and third phases were the most important, diagnosed as having developed in a progressive tectonic process. In the general, more vigorous conditions of PT are related to the interval tardi - phase 2 early-phase 3, whose radiometric ages and regional structuring indicators places it in the Brasiliano/Pan-African Cycle. In the Staterian geodynamic setting of Brazilian Platform , these sequences are correlated to the lower Espinhaço Supergroup (p.ex., Rio dos Remédios and Paraguaçu groups, a paleproterozoic rift system in the São Francisco Craton), the Araí and Serra da Mesa groups (north of Goiás, in the so -called Goiás Central Massif), and the Uatumã Group (in the Amazonian Craton). Granitic ( augen gneisses) plutonics are also known from these areas, as for example the A-type granites intrusive in the Araí and Serra da Mesa groups, dated at 1.77 Ga. Gravimetric and geological data place the limits of the Jaguaribeano System (terranes) along the Senador Pompeu Shear Zone (western border) and the Portalegre- Farias Brito shear zone (eastern and southern). However, the same data area not conclusive as regards the interpretation of those structures as suture of the terrane docking process. The main features of those shear zones and of involved lothological associations, appear to favour an intracontinental transpressional -transcurrent regime, during Neoproterozoic-Cambrian times, marking discontinuities along which different crustal blocks were laterally dispersed. Inside of this orogenic system and according to the magnetic data (total field map), the most important terrane boundary appears to be the Jaguaribe shear zone. The geochronological data, on some tectonostratigraphic associations (partly represented by the Ceará and Jucurutu groups), still at a preliminary level, besides the lack of granitic zonation and other petrotectonic criteria, do not allow to propose tectonic terrane assembly diagrams for the studied area

Sistemas orbitais e aéreos aplicados à análise multi-escala da tectônica rúptil atuante na borda sudeste da Bacia do Parnaíba

The tectonics activity on the southern border of Parnaíba Basin resulted in a wide range of brittle structures that affect siliciclastic sedimentary rocks. This tectonic activity and related faults, joints, and folds are poorly known. The main aims of this study were (1) to identify lineaments using several remotesensing systems, (2) to check how the interpretation based on these systems at several scales influence the identification of lineaments, and (3) to contribute to the knowledge of brittle tectonics in the southern border of the Parnaíba Basin. The integration of orbital and aerial systems allowed a multi-scale identification, classification, and quantification of lineaments. Maps of lineaments were elaborated in the following scales: 1:200,000 (SRTM Shuttle Radar Topographic Mission), 1:50,000 (Landsat 7 ETM+ satellite), 1:10,000 (aerial photographs) and 1:5,000 (Quickbird satellite). The classification of the features with structural significance allowed the determination of four structural sets: NW, NS, NE, and EW. They were usually identified in all remote-sensing systems. The NE-trending set was not easily identified in aerial photographs but was better visualized on images of medium-resolution systems (SRTM and Landsat 7 ETM+). The same behavior characterizes the NW-trending. The NS-and EW-trending sets were better identified on images from high-resolution systems (aerial photographs and Quickbird). The structural meaning of the lineaments was established after field work. The NEtrending set is associated with normal and strike-slip faults, including deformation bands. These are the oldest structures identified in the region and are related to the reactivation of Precambrian basement structures from the Transbrazilian Lineament. The NW-trending set represents strike-slip and subordinated normal faults. The high dispersion of this set suggests a more recent origin than the previous structures. The NW-trending set may be related to the Picos-Santa Inês Lineament. The NS-and EW-trending sets correspond to large joints (100 m 5 km long). The truncation relationships between these joint sets indicate that the EW-is older than the NS-trending set. The methodology developed by the present work is an excellent tool for the understanding of the regional and local tectonic structures in the Parnaíba basin. It helps the choice of the best remote-sensing system to identify brittle features in a poorly known sedimentary basin

Histórias de adoção tardia: considerações a partir da analítica existencial heideggeriana

Adoption establishes a filiation status, resulting from a legal act, which attributes to the child and parents the rights and obligations associated with such condition, being legally irrevocable. Nevertheless, in practice there are adoptions that do not concretize and the child returns to justice during or even after the legal process is closed. Late adoption is the denomination of the adoption of children over two years and it is still permeated by myths and stigmas, leading to a frequent return of the child to justice in these cases. The late adoption involves a process of building a unique relationship with a child whose backstory is commonly marked by the dissolution of the relationship with the family of origin, due to violation of rights and, in some cases, the experience of institutional care. Given such a scenario, this research, based on the Existential Analytic proposed by Martin Heidegger, seeks to understand the experience of mothers and children in the process of late adoption, in order to obtain subsidies to psychological attention in this context. This is a qualitative, phenomenological study with a comprehensive focus. The participants were two mothers and two children who have gone through late adoption for about two years. The procedures of data generation contemplated narrative interviews with mothers and individual meetings with children, in which ludic resources were used as mediators of expression (free drawings, unfinished children's story and "Story-Drawings" on late adoption). The procedures were audiotaped and transcribed. Data analysis was grounded in Heidegger's hermeneutics. The late adoption process, permeated by historical, social and cultural determinants and the web of meanings that create the historical singularity of each person involved have proved to be complex as seen in the narratives. The construction of the meanings of parenthood and filiation has been developing in the families in the study, from the experience of being-with-the-other, caring and dwelling in their peculiar modes of expression. The family of origin and the adoptive family mingle and differentiate by means of the experience of children, especially because of the existence of biological siblings. Data point to the importance of psychological care to family core in late adoption processes

Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.