BT

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.

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