9

Il semble que l'analyseur statique à utiliser avec les contrats de code .NET 4.0 ne sera disponible que pour les éditions Team Suite de Visual Studio - ce qui le place bien en dehors du budget de mon équipe. Y a-t-il des alternatives (open source, gratuites ou à un prix raisonnable) qui offrent une analyse statique similaire pour la conception par code de style de contrat (n'utilisant pas nécessairement des contrats de code .net). Je suppose que la réponse sera non, car la pleine valeur ne vient que lorsque la BCL elle-même a des contrats - mais y en a-t-il qui font partie du chemin?Toute alternative à l'analyseur statique .Net 4 Contracts Code?

Répondre

2

Je ne suis pas sûr que ce soit ce que vous cherchez, mais vous pouvez jeter un oeil à Frama-C et son langage d'annotation ACSL pour C.

Par rapport aux contrats .NET, les contrats de ACSL ne sont pas exécutables (il est impossible de les vérifier avec des assertions d'exécution) mais sont mieux adaptés à l'analyse statique (ils sont plus expressifs et permettent d'écrire et de vérifier statiquement une spécification complète.)

+0

En un coup d'œil, cela semble vraiment impressionnant - surtout avec tous les plugins. Le plugin d'analyse de la valeur en particulier est parmi les choses que je voudrais utiliser. Je vais certainement le vérifier! Je vois que c'est un ensemble d'outils génériques pour tout ce qui se trouve dans la famille C - une expérience de la façon dont elle s'intègre avec C# ou les pièges courants à éviter? – FinnNk

+0

@FinnNk Je ne suis pas sûr de "quoi que ce soit dans la famille C" ... C'est uniquement pour C. L'effort initial était de gérer le C embarqué critique, donc le problème de l'interfaçage C# ou d'autres langages avec leur propre syntaxe pour les contrats complètement ignoré. Et comme il se passe encore beaucoup de choses sur les contrats .NET, ce serait encore un peu prématuré en ce moment, même si cela semble être un sujet intéressant. –

+0

@FinnNk En ce qui concerne les pièges, dans le plug-in d'analyse de valeur, vous constaterez rapidement que le support ACSL est très partiel (même parmi le sous-ensemble d'ACSL pouvant être pris en charge dans une analyse statique de propagation anticipée automatique). En tant que limitation typique, l'analyse de la valeur ne comprend toujours pas les résultats post-conditions. Avez-vous vu le tutoriel de Jessie? Il a quelques spécifications complètes pour des fonctions simples, exprimées en contrats. http://frama-c.cea.fr/jessie_tutorial_index.html –

0

J'utilise l'analyse statique dans VS2010 Prime.