Дафни верификатор: VSCode против вывода командной строки - PullRequest
Новая
       22

Дафни верификатор: VSCode против вывода командной строки

0 голосов
/ 26 марта 2020

Я использую Dafny в Visual Studio Code 1.43.2 для Windows 10.

Мой алгоритм был проверен с примерно 150 проверочными обязательствами. Затем я добавил переменную-призрак и еще несколько лемм, но не изменил алгоритм. Теперь я получаю ошибки тайм-аута для инварианта и условие уменьшений al oop (это было до этого), как показано ниже.

enter image description here

Добавление дополнительных операторов assert или даже assume просто приводит к истечению тайм-аута большего количества инвариантов. Поэтому я попытался запустить Dafny из командной строки вместо параметров /compile:0 (потому что у меня есть два метода без тела) и /tracePOs. Я получаю следующий вывод: 

Verifying CheckWellformed$$_module.__default.Bisimilarity ...         [6 proof obligations]   verified
Verifying Impl$$_module.__default.Bisimilarity ...                    [140 proof obligations] verified
Verifying CheckWellformed$$_module.__default.Calculate ...            [9 proof obligations]   verified
Verifying CheckWellformed$$_module.__default.Sum ...                  [14 proof obligations]  verified
Verifying CheckWellformed$$_module.__default.Split ...                [5 proof obligations]   verified
Verifying CheckWellformed$$_module.__default.Union ...                [3 proof obligations]   verified
Verifying Impl$$_module.__default.AddingPartitions ...                [12 proof obligations]  verified
Verifying Impl$$_module.__default.AllElementsInUnion ...              [6 proof obligations]   verified
Verifying Impl$$_module.__default.UnionOfDifference ...               [6 proof obligations]   verified
Verifying Impl$$_module.__default.EnsureDisjoint ...                  [4 proof obligations]   verified
Verifying Impl$$_module.__default.EnsureSubset ...                    [2 proof obligations]   verified
Verifying Impl$$_module.__default.MaximumPartition ...                [12 proof obligations]  verified
Verifying Impl$$_module.__default.SplittersDecrease ...               [5 proof obligations]   verified
Verifying Impl$$_module.__default.BlockInU ...                        [5 proof obligations]   verified
Verifying Impl$$_module.__default.BlockNotInU ...                     [3 proof obligations]   verified
Verifying CheckWellformed$$_module.__default.OutgoingTransitions ...  [45 proof obligations]  verified
Verifying Impl$$_module.__default.OutgoingTransitions ...             [12 proof obligations]  verified

Dafny program verifier finished with 17 verified, 0 errors

Означает ли это, что алгоритм верен, но объем обязательств по доказательству слишком велик для VSCode? Есть ли способ это исправить? Я попытался изменить файл настроек. json, чтобы увеличить ограничение по времени, но я не уверен, каким было значение по умолчанию, и если это правильный способ сделать это: 

{
    "dafny.basePath": "c:\\Users\\zaina\\.vscode\\extensions\\correctnesslab.dafny-vscode-0.17.1\\dafny\\dafny",
    "[dafny]": {},
    "dafny.serverVerifyArguments" : ["/timeLimit:110"]
}
...