XINFORMAÇÕES SOBRE DIREITOS AUTORAIS
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
Coleção Digital
Título: TECHNIQUES FOR THE USE OF HOARE LOGIC IN PCC Autor: JULIANA CARPES IMPERIAL
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):
EDWARD HERMANN HAEUSLER - ADVISOR
Nº do Conteudo: 4428
Catalogação: 22/01/2004 Idioma(s): PORTUGUESE - BRAZIL
Tipo: TEXT Subtipo: THESIS
Natureza: SCHOLARLY PUBLICATION
Nota: Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4428@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4428@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.4428
Resumo:
Título: TECHNIQUES FOR THE USE OF HOARE LOGIC IN PCC Autor: JULIANA CARPES IMPERIAL
Nº do Conteudo: 4428
Catalogação: 22/01/2004 Idioma(s): PORTUGUESE - BRAZIL
Tipo: TEXT Subtipo: THESIS
Natureza: SCHOLARLY PUBLICATION
Nota: Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4428@1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=4428@2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.4428
Resumo:
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.