проверка инварианта с использованием контрактов кода Microsoft

Question

Только что получил контракты Microsoft Code на проверку предварительных, постусловных и объектных инвариантов в коде (https://docs.microsoft.com/en-us/dotnet/framework/debug-trace-profile/code-contracts)) и хотел бы попробовать его. Один вопрос, который я хотел бы подтвердить относительно надежности и Полнота, учитывая инвариант, предполагая, что средство проверки не выводит никаких сообщений об ошибках, означает ли это, что инвариант действительно (доказуемо) истинен, или он все еще может быть ложно-положительным.

Answer 1

Статическую проверку можно обмануть различными способами, например, добавив ложное предположение. В этом ответе я предполагаю, что ничего подобного не было сделано.

Также возможно, что в контролере есть ошибки. Но при условии, что их нет ...

Статическая проверка предназначена для получения ложных срабатываний. Все предварительные и постусловия и инварианты будут проверены, и они пройдут только в том случае, если истинность условий может быть подтверждена положительно. Если условие не может быть проверено, будет выдано сообщение об ошибке.

Система не будет пытаться доказать, что инвариант может быть нарушен. «Недоказанное» сообщение об ошибке означает, что доказательств правильности не найдено. Инвариант все еще может быть истинным, просто недоказанным.

Таким образом, нет ложных срабатываний (опять же, по замыслу, при условии отсутствия ошибок или саботажа).