Made available in DSpace on 2014-12-17T15:47:48Z (GMT). No. of bitstreams: 1
ClaudiaFCKT.pdf: 525104 bytes, checksum: 174fb60f1cf9ebfc609d837f2787b6b1 (MD5)
Previous issue date: 2007-07-27 / 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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/17984 |
| Date | 27 July 2007 |
| Creators | Tavares, Cl?udia Fernanda Oliveira Kiermes |
| Contributors | CPF:00809085437, http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5, Abrantes, Jorge C?sar, CPF:47486196487, http://lattes.cnpq.br/1424808046858622, D?harbe, David Boris Paul |
| Publisher | Universidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Sistemas e Computa??o, UFRN, BR, Ci?ncia da Computa??o |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0021 seconds