BT

Spec# e Boogie Disponíveis no CodePlex

| por Jonathan Allen , traduzido por Marcus Rehm em 02 set 2009. Tempo estimado de leitura: 1 minuto |

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

Faça seu login para melhorar sua experiência com o InfoQ e ter acesso a funcionalidades exclusivas


Esqueci minha senha

Follow

Siga seus tópicos e editores favoritos

Acompanhe e seja notificados sobre as mais importantes novidades do mundo do desenvolvimento de software.

Like

Mais interação, mais personalização

Crie seu próprio feed de novidades escolhendo os tópicos e pessoas que você gostaria de acompanhar.

Notifications

Fique por dentro das novidades!

Configure as notificações e acompanhe as novidades relacionada a tópicos, conteúdos e pessoas de seu interesse

BT