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.

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

We notice you’re using an ad blocker

We understand why you use ad blockers. However to keep InfoQ free we need your support. InfoQ will not provide your data to third parties without individual opt-in consent. We only work with advertisers relevant to our readers. Please consider whitelisting us.