BT
x Por favor preencha a pesquisa do InfoQ !

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.

Avalie esse artigo

Relevância
Estilo/Redação

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
Feedback geral
Bugs
Publicidade
Editorial
Marketing
InfoQ Brasil e todo o seu conteúdo: todos os direitos reservados. © 2006-2016 C4Media Inc.
Política de privacidade
BT

Percebemos que você está utilizando um bloqueador de propagandas

Nós entendemos porquê utilizar um bloqueador de propagandas. No entanto, nós precisamos da sua ajuda para manter o InfoQ gratuito. O InfoQ não compartilhará seus dados com nenhum terceiro sem que você autorize. Procuramos trabalhar com anúncios de empresas e produtos que sejam relevantes para nossos leitores. Por favor, considere adicionar o InfoQ como uma exceção no seu bloqueador de propagandas.