[pt] Esta dissertação apresenta os dados de um teste de carga instrumentado em um cais, enfatizando a importância da instrumentação de campo para melhor compreender o comportamento da estrutura durante o teste. Dentro desta abordagem, foi realizada uma revisão sobre o comportamento de grupo de estacas, direcionada à influência do espaçamento entre estacas na interação entre as mesmas, e da rigidez do bloco na distribuição de carga entre as estacas, no fator de segurança das mesmas e das distorções angulares do bloco. Em seguida, foram descritas as características geométricas e geotécnicas do cais testado, e foram apresentadas as características da instrumentação utilizada, composta por extensômetros elétricos, eletroníveis e nível topográfico, desde sua montagem e calibração, até a sua instalação em campo. Foi destacada a utilização dos eletroníveis, que apesar de pouco utilizados na prática da engenharia geotécnica, são instrumentos versáteis, precisos e podem ser reutilizados. O procedimento do teste de carga foi realizado de modo a simular a situação real da maneira mais próxima da realidade, onde foram monitoradas as deformações em quatro estacas, a rotação e o recalque da laje do cais. A estrutura apresentou bom desempenho durante o teste, com baixo nível de deformação nas estacas, distorção angular desprezível e baixos valores de recalque total e residual. / [en] This dissertation presents the data of an instrumented load test in a wharf, emphasizing the importance of field instrumentation to analyze the behavior of the structure during the load test. First, a review was carried out on the behavior of pile groups, focusing on the influence of pile spacing in the interaction factors. It also considered the influence of the raft stiffness on the load distribution and factor of safety of the piles. The main characteristics of the wharf were presented, such as, geometry, dimensions, deformability and strength properties of the concrete. The geological and geotechnical subsoil profile have been presented, indicating a soft clay layer resting on a very compact residual soil. The particularities of the instrumentation used on the test, composed by strain gauges, electrolevels and a topographic level, were presented since the assembly and calibration, to the installation on field. Despite its underutilization in geotechnical engineering practice, the use of electrolevels was emphasized, due to its versatility, accuracy and the fact that they can be reutilized. The load test procedure was made to simulate the real situation as close as possible, where strain in four piles, rotation and settlement of the deck were monitored. The structure performanced well during the test, presenting low level of strain in piles, negligible angular distortion of the deck and low values of total and residual settlements.

[pt] Prova automática de teoremas consiste na prova de teoremas matemáticos por intermédio de programas de computador. Dependendo da linguagem lógica em uso, o processo de provar uma determinada fórmula pode não ser computável. Além disso, dependendo do cálculo dedutivo empregado, a busca por uma prova envolve lidar com a possibilidade de aplicação de longas sequências de axiomas e regras de inferência. Tudo isso reforça a necessidade da intervenção humana no processo de prova em sistemas denominados provadores interativos de teoremas ou assistentes de prova. Em um cenário típico, um usuário interage com a máquina de prova através de uma interface gráfica, normalmente implementada como um aplicativo desktop. Recentemente, porém, muitos aplicativos deste tipo passaram a ser oferecidos para seus usuários através da web. Esta forma de disponibilizar software evita que o usuário final se preocupe com questões de instalação e configuração e possibilita o acesso ao sistema de qualquer computador, com qualquer sistema operacional, bastando ter disponível uma conexão com a Internet. Nesta dissertação, estudamos possibilidades de uso da web como plataforma para a construção de ambientes interativos para prova de teoremas. Nossa proposta é estudar os diferentes modelos de interação entre usuário e ambientes de prova automatizados e verificar como estes modelos podem ser adaptados para a web. Como resultado, apresentamos uma ferramenta gráfica para visualização e manipulação direta de provas formais na web como uma interface alternativa entre usuários e provadores. / [en] Automatic theorem proving consists of proving mathematical theorems by means of computer programs. Depending on the logic used, the process of proving a formula is not computable. Moreover, depending of the deductive system applied to, the search for a proof can involve the application of long sequences of axioms and inference rules, reinforcing the need of human intervention in the proof process. Such systems are known as interactive theorem provers or proof assistants. In a typical scenario, the user interacts with the prover through a graphical interface, usually a desktop application. Recently, however, applications like those started to be delivered to users through the web. This way of software deployment avoids that final users have to deal with complex activities like prover installation and configuration and allows this user to access the system from different machines with a simple Internet connection. In this research we study the use of web as a platform for interactive theorem proving environments construction. Our purpose is to study some interaction models between user and automated proof environments and verify how these models can be adapted to work as a web application. As a result we show a graphical tool for visualization and direct manipulation of formal proofs on web to work as an alternative interface between user and proving machines.

[pt] Ao menos desde 1916, a quitação é um instituto típico do Direito Privado brasileiro. Mas é certo que, muito antes disso, a quitação já era um instrumento socialmente típico e de absoluta relevância, com presença marcante no tráfico negocial. Apesar da sua importância prática, o instituto da quitação carece de trabalhos monográficos específicos a seu respeito. E custa caro aos tribunais brasileiros a inexistência de um estudo dedicado à sistematização do instituto e ao estabelecimento de parâmetros interpretativos para as situações em que o alcance da eficácia da quitação é objeto de controvérsia. Somente na Segunda Seção do Superior Tribunal de Justiça – órgão fracionário de elevada hierarquia dentro da Corte nacional que tem exatamente a função de uniformizar a jurisprudência – há entendimentos conflitantes sobre a interpretação da quitação que geram insegurança e incerteza ao jurisdicionado quanto aos critérios a serem analisados pelo intérprete para autorizar ou não a investida judicial para ver complementada uma obrigação já anteriormente quitada. Nesse cenário, com o objetivo de, em alguma medida, preencher tal lacuna doutrinária, este trabalho analisará o instituto da quitação de forma sistematizada à luz da legislação brasileira, abordará o seu perfil funcional, examinará precedentes do Superior Tribunal de Justiça que revelam séria divergência e buscará oferecer parâmetros interpretativos para os impasses a respeito do alcance da quitação. / [en] At least since 1916, the discharge is a typical institute of Brazilian Private Law. However, it is certain that, long before that, discharge was already a relevant and socially typical instrument, continuously present in business traffic. Despite its practical importance, the discharge institute lacks specific monographic works about it. And it is costly to the Brazilian courts that there is no study dedicated to systematizing the institute and establishing interpretative parameters for situations in which the scope of the effectiveness of the discharge is a controversial topic. For example, in the Second Section of the Brazilian Superior Court of Justice – a hierarchically high part within the national Court that has the exact function of standardizing the jurisprudence – there are conflicting understandings on the interpretation of the discharge that create insecurity and uncertainty for the person subject to its jurisdiction related to the criteria to be analyzed by the interpreter in order to authorize or not the judicial onslaught to see a previously settled obligation complemented. In this scenario, with the objective of, to some extent, filling this doctrinal gap, this work will analyze the institute of discharge in a systematized way in light of the Brazilian law system, address its functional profile, examine precedents of the Superior Court of Justice representing serious divergence and seek to offer interpretative parameters for certain impasses regarding the scope of the discharge.

[pt] O advento do uso maciço de computadores em provas matemáticas, ocorrido ao final da década de setenta com a solução de um famoso problema matemático – a prova do Teorema das Quatro Cores – ocasionou disputas filosóficas que ainda hoje demandam esclarecimentos. O objetivo principal da tese consiste em elaborar alguns dos referidos esclarecimentos desde uma perspectiva motivada pela filosofia da matemática de Ludwig Wittgenstein, especialmente no que diz respeito à distinção continuamente manuseada e depurada pelo filósofo ao longo do desenvolvimento de seu pensamento entre provas e experimentos. Após apresentar as principais ideias da prova do Teorema das Quatro Cores em termos históricos, algumas distinções conceituais metodologicamente significativas são elaboradas. A seguir o trabalho analisa, a partir da concepção funcional de a priori de Arthur Pap, o argumento da introdução da experimentação nas matemáticas de Thomas Tymoczko. A leitura das controvérias filosóficas que se seguiram ao argumento de Tymoczko é então apresentada, aplicando-se as distinções conceituais anteriormente elaboradas. Por fim algumas ideias wittgensteinianas sobre da disitinção entre provas e experimentos são exploradas em conexão com a noção de sinopticidade de provas, considerando menos os papéis específicos de tais noções na filosofia da matemática de Wittgenstein, do que investigando as vantagens de suas possíveis aplicações no esclarecimento de tópicos críticos das referidas disputas. / [en] The massive use of computers in mathematical proofs, which started in the end of the seventies trough the solution of one famous mathematical problem – the Four-Color Theorem – entailed philosophical disputes still in need of elucidation. The central aim of this thesis consists in elaborating some of these elucidations from a point of view motivated by Ludwig Wittgenstein’s philosophy of mathematics, mainly in what concerns the distinction between proofs and experiments, which was continuously used and elaborated by the philosopher in the course of the development of his thought. After the presentation of the main ideas involved in the proof of the Four-Color Theorem from a historical perspective, some methodological conceptual distinctions are elaborated. The thesis then shifts to an analysis of the introduction of experiment in mathematics argument, by Thomas Tymoczko, from the point of view of Arthur Pap’s conception of functional a priori. An interpretation of the controversies that followed that argument is developed trough the application of the conceptual distinctions previously elaborated. At last, some wittgensteinian ideas about the distinction between proofs and experiments are explored in connection with the notion of surveyability of proofs, concerned less with its specific roles in Wittgenstein’s philosophy of mathematics than with investigating the advantages of its possible applications in the elucidation of some critical points in the referred controversies.

[pt] Nas últimas duas décadas o governo brasileiro tem investido vultosos recursos para promover o acesso às tecnologias de informação e comunicação nas escolas públicas do país. Os instrumentos normativos (decretos, leis, portarias) que instituem tais políticas enunciam como objetivo principal a melhoria da aprendizagem dos alunos, a partir do uso pedagógico de computadores, Internet e outros aparatos que se tornaram cotidianos a partir da sociedade da informação. Neste trabalho investigamos possíveis correlações entre o uso de TIC em escolas públicas brasileiras e o resultado médio destas mesmas escolas em testes de proficiência de larga escala. Para isso nos baseamos nos resultados da Prova Brasil 2011, e nos dados levantados, no mesmo ano, pela pesquisa TIC Educação; realizada pelo Comitê Gestor da Internet no Brasil. Neste segundo caso foram considerados os questionários aplicados a professores de quinto e nono anos do ensino fundamental, a partir dos quais foram desenvolvidos dois indicadores do uso pedagógico de TIC por professores, o que permitiu, posteriormente, medir o uso de TIC por escola. Os indicadores foram construídos a partir de modelos estatísticos utilizando a Teoria de Resposta ao Item (TRI). / [en] In the last two decades, the brazilian government has invested huge resources to promote the access to the information and communication technologies at the public schools. The regulatory instruments which establish such policies indicate as a major objective, the improvement of the student s academic achievement, from the educational use of computers, Internet, and other tool which are used daily, in the information society context. In this work we investigate possible correlations between the ICT use at brazilian public schools, and the results of these same schools in the national test of academic achievement. Our start point are the results of Prova Brasil 2011, and the data collected in the same year, by the TIC Educação, research realized by the Brazilian Internet Steering Committee. In the case of this second process, we have considered the interviews applied to the teachers of fifth and ninth year, of the basic level, from what was developed two indexes to measure the educational ICT use for each school. These indexes were developed from statistical models, using the Item response theory.

[pt] Este trabalho tem por objetivo investigar as demandas de processamento relacionadas à resolução de provas de língua portuguesa do SAERJinho, focalizando-se, em particular, fatores de ordem linguístico-textual envolvidos na leitura de textos e enunciados das referidas provas. Na resenha da literatura são apresentadas vertentes teóricas sobre o processamento da leitura, seus aspectos cognitivos, metacognitivos assim como os conceitos de legibilidade e inteligibilidade. Dada a multiplicidade semiótica que caracteriza os textos das provas analisadas, são considerados os conceitos de multimodalidade e multiletramento. Apresenta-se, adicionalmente, literatura relativa a gêneros textuais, tendo em vista a identificação dos gêneros mais recorrentes nas provas examinadas. Uma breve caracterização dos tipos de questão de múltipla escolha usados em provas objetivas também é estabelecida, entendendo-se que aspectos metacognitivos associados à resolução desses tipos de questão podem afetar o desempenho dos alunos nas provas. A fim de compreender os critérios de elaboração das provas, foram considerados os Parâmetros Curriculares Nacionais para o Ensino Médio, que são a base referencial da Matriz de Referência utilizada na elaboração do SAERJinho. Antes das análises, o SAERJinho foi apresentado. No capítulo da metodologia, são apresentados o corpus da pesquisa, a ferramenta usada para verificar o grau de legibilidade dos textos (Coh-Metrix-Port) e o valor do índice Flesch associado a cada texto. Em seguida, procedeu-se à análise dos gêneros textuais, dos tipos de questão de múltipla escolha e também das habilidades e dos conteúdos específicos cobrados nas questões. Os resultados da pesquisa sinalizaram para a necessidade de se reavaliarem os critérios de elaboração das provas e apontaram ainda para a necessidade urgente de os alunos do Ensino Médio desenvolverem as habilidades necessárias para alcançarem proficiência em leitura (como por exemplo, inferir uma informação implícita em um texto, identificar o tema de um texto, identificar a finalidade de textos de diferentes gêneros) e, consequentemente, terem bom êxito nas avaliações. / [en] This thesis is aimed at investigating the processing demands related to taking the SAERJinho s Portuguese Language Tests (the Education Evaluation System of the State of Rio de Janeiro), by focusing, in particular, on textual-linguistic factors involved in reading the statements of the mentioned tests. In the literature review, we present the theoretical framework for reading processing, its cognitive and metacognitive aspects, as well as the concepts of readability and intelligibility. Due to the semiotic multiplicity that characterizes the texts of the tests analyzed, the concepts of multi-modality and multi-literacy are considered. Additionally, we present the literature regarding text genres, focusing on the identification of the most recurrent genres in the tests examined. A brief characterization of the types of multiple choice questions used in objective tests is also established, bearing in mind that metacognitive aspects associated with the resolution of these types of question may affect students performance on the tests. In order to understand the criteria involved in test preparation, we consider the Brazilian National Curriculum Parameters for the Secondary Education, which are the reference basis of the Reference Matrix used in the preparation of the SAERJinho. Before showing the analyses, the SAERJinho is introduced. In the methodology chapter, the research corpus is shown, as well as the tool used to verify the readability level of the texts (Coh-Metrix-Port) and the Flesch reading score associated with each text. Then, we analyze the text genres, the types of multiple choice questions and also the skills and the specific topics covered in the questions. Research results show that it is necessary to re-evaluate the criteria involved in the elaboration of the tests and they also point out that high school students should urgently develop their reading proficiency (such as, for example, inferring implicit information in a text, identifying the text s topic and the purpose of texts of different genres) and, consequently, achieve good results in the evaluations.

[pt] O presente estudo teve como principal objetivo demonstrar que fibras derivadas da reciclagem de garrafas PET (Polietileno Tereftalato), confeccionadas com 100 porcento do resíduo, pela indústria têxtil, podem ser uma boa alternativa se utilizadas como reforço de solos, quando submetidos a diferentes níveis de cargas. Buscando uma melhor aplicabilidade para este material, foram executados ensaios de compressão triaxial drenados em laboratório, bem como ensaios de prova de carga em placa e também com simulação de um talude em modelo físico reduzido, para a determinação do comportamento mecânico de uma areia e do compósito areia-fibras PET. Para os ensaios triaxiais drenados, foram utilizadas fibras PET com dois títulos (correspondente ao diâmetro das fibras) e comprimentos distintos (1,4 dtex com 38 mm e 3,3 dtex com 56 mm), inseridas aleatoriamente na massa de solo, onde foi utilizado o teor de 0,5 porcento de fibras, em relação ao peso seco do solo, teor de umidade de 10 porcento e densidade relativa de 50 porcento. Os resultados mostraram que o comportamento da areia pura é influenciado pela adição de fibras PET, melhorando os parâmetros de resistência, como o intercepto coesivo e o ângulo de atrito, definidos pelo critério de Mohr-Coulomb. O compósito reforçado com as fibras PET de menor título e menor comprimento apresentou um maior ganho na resistência ao cisalhamento, mas ambos os compósitos, em comparação ao solo não reforçado, apresentaram uma maior resistência. Para os ensaios de prova de carga em placa e para a simulação do talude, ambos realizados em modelo físico reduzido, foram utilizadas as fibras de menor título e menor comprimento como elemento de reforço. Observa-se que a inserção das fibras PET melhora o comportamento carga-recalque da areia pura, onde o compósito reforçado apresenta uma maior capacidade de suporte e a redução dos recalques, bem como uma mudança na propagação e formação das fissuras ao redor da placa. Na simulação do talude, a inserção das fibras PET promove uma alteração completa no mecanismo de ruptura ocorrido no compósito, quando comparado à ruptura da areia pura. Ressalta-se o emprego positivo das fibras PET para aplicação como reforço de solos em obras geotécnicas (como por exemplo, em camadas de aterros sanitários, aterros sobre solos moles, reforço de taludes, base de fundações superficiais e controle de erosão), além de eliminar problemas atuais de disposição de resíduos, dando um fim mais nobre a este material, com benefícios ambientais, sociais e econômicos. / [en] The main objective of this study was to demonstrate that fibers derived from the recycling of PET (Polyethylene Terephthalate) bottle, 100 percent made from the residue by the textile industry, can be a good alternative if used as reinforcement of soil, when submitted to different load levels. Looking for a better applicability for this material, were executed drained triaxial compression tests in laboratory, as well as plate load tests, also with slope simulation in a reduced physic model, to evaluate the mechanical behavior of a sand and a composite sand-PET fibers. For the drained triaxial tests, were used PET fibers with two different titles (corresponding to the fiber diameters) and lenghts (1,4 dtex com 38 mm e 3,3 dtex com 56 mm), distributed randomly in the soil mass, where was used a fiber contente of 0,5 percent by relation to the soil s dry weight, moisture content of 10 percent and relative density of 50 percent. The results showed that the pure sand behavior was influenced by the addition of PET fibers, improving the strenght parameters as the cohesion intercept and the friction angle, defined by the Mohr-Coulomb criteria. The composite reinforced with PET fibers with minor title and lenght presented a better improvement in the shear strenght, but both composites, compared to the non reinforced soil, showed greater resistence. For the plate load tests and for the slope simulation, both performed in a reduced physic model, it was used the fiber with minor title and lenght as reinforcement element. The addiction of PET fibers improve the load-settlement behavior of the sand, where the reinforced composite shows a greater bearing capacity, a reduction of the settlements and a change in the propagation and formation of fissures around the plate. In the slope simulation, the addiction of PET fibers promove a complete alteration in the rupture mechanism that occurred in the composite, when compared to the rupture of the pure sand. It is highlighted the positive use of PET fibers for application as soil reinforcement in geotechnical works (as an example, in landfill layers, embankment on soft soil, slope reinforcement, base of shallow foundations and erosion control), eliminating current problems of waste disposal, giving a noble end to this material, with environmental, social and economical benefits.

[pt] Segerberg apresentou uma prova geral da completude para lógicas proposicionais. Para tal, um sistema de dedução foi definido de forma que suas regras sejam regras para um operador booleano arbitrário para uma dada lógica proposicional. Cada regra desse sistema corresponde a uma linha na tabela de verdade desse operador. Na primeira parte desse trabalho, mostramos uma extensão da ideia de Segerberg para lógicas proposicionais finito-valoradas e para lógicas não-determinísticas. Mantemos a ideia de definir um sistema de dedução cujas regras correspondam a linhas de tabelas verdade, mas ao invés de termos um tipo de regra para cada valor de verdade da lógica correspondente, usamos uma representação bivalente que usa a técnica de fórmulas separadoras definidas por Carlos Caleiro e João Marcos. O sistema definido possui tantas regras que pode ser difícil trabalhar com elas. Acreditamos que um sistema de cálculo de sequentes definido de forma análoga poderia ser mais intuitivo. Motivados por essa observação, a segunda parte dessa tese é dedicada à definição de uma tradução entre cálculo de sequentes e dedução natural, onde procuramos definir uma bijeção melhor do que as já existentes. / [en] Segerberg presented a general completeness proof for propositional logics. For this purpose, a Natural Deduction system was defined in a way that its rules were rules for an arbitrary boolean operator in a given propositional logic. Each of those rules corresponds to a row on the operator s truth-table. In the first part of this thesis we extend Segerbergs idea to finite-valued propositional logic and to non-deterministic logic. We maintain the idea of defining a deductive system whose rules correspond to rows of truth-tables, but instead of having n types of rules (one for each truth-value), we use a bivalent representation that makes use of the technique of separating formulas as defined by Carlos Caleiro and João Marcos. The system defined has so many rules it might be laborious to work with it. We believe that a sequent calculus system defined in a similar way would be more intuitive. Motivated by this observation, in the second part of this thesis we work out translations between Sequent Calculus and Natural Deduction, searching for a better bijective relationship than those already existing.

[pt] As alterações no solo decorrentes de um elemento de fundação profunda e seus desempenhos sob a aplicação de carga axial são processos há muito tempo estudados na engenharia civil. Diversos fatores como, método de instalação utilizado, formato da estaca, interações solo-estrutura, mecanismos de transferências de carga, movimentação do solo e alterações na compressibilidade e tensões do solo adjacente, apresentam desafios importantes que ainda não foram totalmente compreendidos nos fenômenos de penetração e capacidade de suporte em estacas. Diversos avanços foram realizados ao longo das últimas décadas para se investigar estes comportamentos, a partir procedimentos experimentais e novas formas de instrumentação, assim como ferramentas numéricas sofisticadas com o emprego de complexos modelos constitutivos em elementos finitos. Apesar destes avanços, a modelagem numérica dos processos citados, com todas as suas complexidades, ainda encontra alguns desafios. Devido a facilidade em lidar com simulações de grandes deformações e de captar o comportamento dilatante e nãolinear de solos granulares, o Método dos Elementos Discretos apresenta uma excelente ferramenta para investigar estes processos, sem grandes complicações. O presente trabalho procurou avaliar os comportamentos obtidos a partir de diferentes processos de instalação da estaca e seus efeitos nos resultados da prova de carga estática em solos granulares. As alterações de tensão e deslocamento foram avaliadas nos diferentes modelos e discutindo sobre uma metodologia básica para obter correspondências qualitativas e quantitativas com os diferentes comportamentos de campo e laboratório. Para este estudo foram utilizados os programas PFC, na versão 2D, e o programa UDEC, da Itasca co. / [en] The disturbances experienced by the soil owing to the load applied to a deep foundation and its relative behavior consist of long time studied phenomena in civil engineering. Several factors such as the installation methods, the pile geometry, the interactions between soil and structure, the load-transfer mechanisms, the soil movements and the disturbances in the stress and compressibility fields present major challenges that have not yet been completely understood. Numerous advances have been observed throw-out the last decades, in order to investigate these behaviors starting from the different pile instrumentations, the use of calibration cameras and centrifuges and most recently the measurement of the stress and strain fields inside the soil mass in model tanks. Despite the advances the numerical modelling of those processes still faces major challenges. Due to simplified approach used by the Discrete Element Method to simulate large deformation and the dilant non-linear behavior of granular soils, it presents as an excellent tool to investigate these processes without further complications. The present work proposed to evaluate the different behaviors obtained with the variations of installation methods investigated as well as their effects in the results of the Pile Load Test. The disturbances were also evaluated in the different models considered and a basic method to achieve qualitative and quantitative comparisons was discussed. These studies were made possible with the help of the PFC2D and UDEC programs developed by Itasca co.

[pt] Atualmente, a maioria dos programas para computadores é obtida através da WEB. Como muitas vezes a procedência são fontes desconhecidas, é preciso se certificar de que o código se comporta como o esperado. A solução ideal seria verificar o código contra uma especificação de políticas de segurança ,contudo, isso pode consumir muito tempo.Uma outra alternativa é fazer com que o próprio código prove ser seguro. O conceito de proof-carryng code (PCC)é baseado nessa idéia : um programa carrega consigo uma prova de sua conformidade com certas políticas de segurança. Ou seja ,ele carrega uma prova a respeito de propriedades do próprio código. Portanto, os mesmos métodos froamsi usados para a verificação de programs podem se utilizados para esta tecnolgia. Considerando este fato,neste trabalho é estudado como cálculo de Hoare, em método formal para realizar a verificação de programas, aplicado a códigos-fonte escritos em uma linguagem de programação imperativa, pode ser útil á tecnica de PCC. Conseqüentemente, são pesquisados métodos para a geração de provas de correção de programas utilizando o método citado, para tornar possível a geração de provas de segurança para PCC utilizando o cálculo de Hoare. / [en] Nowdays most computer programs are obtained from the WEB. Since their source is usually unknown, it is necessary to be sure that the code of the program behaves as expected.The ideal solution would be verify the code against a specification of safety policies.However, this can take too much time.Another approach is making the code itself prove that it is safe. The concept os proof-carryng code (PCC) is based on this idea: a program carries a proof of its conformity with certain safety policies. That is , it carries a proof cencerning properties related to the code itself. Therefore, the same formal methods employed in formal verification of programs can be used in this tecnology. Due to this fact, in this work it is studied how Hoare logic applied to source codes written in an imperative programming language, which is a formal methods are researched to generate proofs of program correctness using the method explained, so that it can be possible to generate PCC safety programs with Hoare logic.