BT

Disseminando conhecimento e inovação em desenvolvimento de software corporativo.

Contribuir

Tópicos

Escolha a região

Início Notícias Spec# e Boogie Disponíveis no CodePlex

Spec# e Boogie Disponíveis no CodePlex

Favoritos

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.

Avalie esse artigo

Relevância
Estilo/Redação

Conteúdo educacional

BT