Il y a certains contrats que je sais que l'analyseur statique ne peut pas prouver. Je peux exclure certains types d'erreurs de violation de contrat d'une fonction entière, mais cela est trop large. Je peux exclure certaines erreurs de violation en utilisant la fonctionnalité baseline.xml, bien que cela soit essentiellement impossible à auditer ou à documenter dans un environnement d'équipe.Puis-je exclure facilement certains contrats de l'analyse statique?
En bref, est-il possible de faire quelque chose comme
Contract.Requires(DoesHalt() == true, ExcludeFromStaticAnalysis=true);
Il y a aussi certains contrats conclus dans les bibliothèques 3e parties qui semblent être mortes pour l'extrémités analyseur statique. Je voudrais les désactiver pour l'analyse statique. Un exemple préféré est un contrat construit pour une bibliothèque de graphes .NET. L'argument d'une première fonction de recherche en profondeur spécifiant quel sommet dans le graphique pour commencer la recherche a un Contract.Requires qui exige que le sommet soit un membre du graphique. Contrat sensible, peut-être même utile d'exécuter dans une version de débogage, mais loin d'être statiquement prouvable. Pourtant, chaque fois que j'utilise la première recherche de profondeur, je dois trouver un moyen d'ignorer la violation statique. Sans la possibilité de partitionner des éléments prouvables à partir de choses non prouvables, je trouve que l'analyse statique est trop bruyante, même avec une petite base de code propre.
Pourquoi ne pouvez-vous pas simplement écrire "Contract.Requires (DoesHalt() = true ou AssumeTrueBecauseYouCantProveThis)"? [où AssumeTrueBecauseYouCantProvethis est une valeur const statique de "true"]. Tout bon «prouveur» devrait être heureux qu'une partie de la disjonction soit trivialement vraie et cesser de travailler sur la vérification du contrat à ce moment-là. –
Parce que le vérificateur d'exécution doit effectuer la vérification. Le contrôle réussirait toujours avec le '|| vrai'. –