BT

LINQ para Z3, O Mais Rápido Comprovador de Teoremas do Mundo

por Jonathan Allen , traduzido por Lucas Souza em 29 Nov 2010 |

A Microsoft Research afirma que o Z3 é o mais rápido comprovador de teoremas do mundo. Z3 está projetado para ser uma ferramenta de baixo nível para outras aplicações, isso não quer dizer stand-alone. Com seu host de comprovadores de teoremas, ele é usado por inúmeros projetos incluindo Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, e HAVOC.

Usando a API .NET do Z3, você pode codificar teoremas usando um estilo orientado a objetos. Entretanto o exemplo no Tutorial do Z3 é demonstrado que mesmo com pequenos problemas pode ser chato codificar.  Bart De Smet gentilmente simplificou isto encapsulando o estilo OO da API com uma API em estilo de queries chamada LINQ para Z3. Abaixo está um exemplo que acompanhou a entrevista de Bart De Smet no canal 9.

  var theorem = from t in ctx.NewTheorem

O suporte ao Z3 está disponível em um primeiro momento no Windows, mas existe uma versão para Linux do Z3. O Z3 está liberado para uso não comercial sob a “Microsoft Research License Agreement”. Você pode vê-lo em ação em uma versão on-line do Z3 no RiSE4fun.

Olá visitante

Você precisa cadastrar-se no InfoQ Brasil ou para enviar comentários. Há muitas vantagens em se cadastrar.

Obtenha o máximo da experiência do InfoQ Brasil.

Dê sua opinião

HTML é permitido: a,b,br,blockquote,i,li,pre,u,ul,p

Receber mensagens dessa discussão
Comentários da comunidade

HTML é permitido: a,b,br,blockquote,i,li,pre,u,ul,p

Receber mensagens dessa discussão

HTML é permitido: a,b,br,blockquote,i,li,pre,u,ul,p

Receber mensagens dessa discussão

Dê sua opinião

Conteúdo educacional

Feedback geral
Bugs
Publicidade
Editorial
InfoQ Brasil e todo o seu conteúdo: todos os direitos reservados. © 2006-2014 C4Media Inc.
Política de privacidade
BT