Spec# e Boogie Disponíveis no CodePlex

por Jonathan Allen , traduzido por Marcus Rehm em 02 Set 2009 |

Spec# é uma linguagem experimental baseada em C#. Spec# é baseada em principios de contrato onde as pre e pós condições necessárias para execução das funções podem ser definidas através de declarações. Outras características incluem "class invariant", referência de tipos não nulos e capacidade aprimorada de análise estática.

Enquanto os Contrato de Código estão incluídos no .NET 4.0, Spec# foi perdendo a força. O código fonte da linguagem está disponível no CodePlex pela Microsoft Research Shared Source License Agreement. Esta licença restringe a utlização para fins não comerciais.

Andando ao lado do Spec# está o Boogie, uma linguagem intermediária para verificação de código. Boogie não é especificamente para .NET, outras linguagens que suportam incluem “a HAVOC e verificadores vcc para C, a linguagem Dafny e verificador, e a linguagem concorrente Chalice”.

Boogie também é o nome de uma ferramenta. Esta ferramenta aceita a linguagem Boogie como entrada, opcionalmente infere algumas invariantes no programa Boogie e então gera condições de verificação que são enviadas para um SMT. O SMT padrão é o Z3.

Boogie foi lançada pela Microsoft Public License, a qual está em conformidade com o padrão Free/Open Source.

Atualmente a Microsoft está posicionando o Contrato de Código (Code Contracts) como o caminho escolhido, isso significa que Spec# não terá muito futuro no mundo do desenvolvimento.