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.