添加需要子句时验证时间减少 [英] Verification Time Decreased when Adding Requires Clauses

问题描述

我正在做一项研究，包括收集不同级别规格的验证时间。我注意到在添加前置条件时，具有不变量的类的验证时间会减少。这是因为当添加前置条件时，验证者的搜索空间更受约束
？这是我的猜测，并希望对此有更深入的了解。

I'm doing a study that include collecting verification time for different level of Specs. I noticed a decrease in the verification time of a class with invariants when preconditions are added. Is this because the search space for the verifier is more constrained when preconditions are added? This is my guess and would appreciate more insight on that.

 

谢谢！

  ;

Iman

推荐答案

嗨伊曼，

 对的，这是可能的。您放置的合同越多，您对静态检查器的帮助就越多，因此验证时间会缩短。

  yes, it is possible. The more contracts you put, the more you help the static checker, so that verification time should go down.

我很乐意帮助您完成学习，所以不要想更多问题。

I will be happy to help with your study, so o not esitate to ask more questions.

 

ciao，

f

这篇关于添加需要子句时验证时间减少的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！