Есть ли программное обеспечение для проверки модели (например, Java Path Finder), но для C#?

Question

< EDIT> Об этом вопросе, не относящемся к теме и слишком основанном на мнениях, я постараюсь быть более ясным. Моя цель состояла в том, чтобы разобраться, если такой инструмент существует, меня не интересовали мнения о том, что было лучшим. В то время, когда я написал этот вопрос, я потратил немало времени на поиск в Интернете и нашел только старые мертвые проекты, но такой инструмент для Java существовал, и я не мог поверить, что ничего не было для C#. Я думаю, что этот вопрос связан с программированием (проверка кода), и на самом деле он не просит мнения. Кроме того, все еще нелегко найти эту информацию, и я думаю, что мой ответ может помочь спасти чье-то время. Тем не менее, я не эксперт stackoverflow, если вы все еще думаете, что вопрос/ответ не подходит для сайта, не стесняйтесь его удалять. < /EDIT>

Я нашел луноход http://fmt.cs.utwente.nl/tools/moonwalker/ но последнее обновление было сделано в 2009 году, и я не думаю, что он поддерживает .net4.5 (и это плохо документированы).

Ответ на этот вопрос предлагает CodeContracts как средство проверки модели Model checking tool c#, но я попытался использовать его, и я не думаю, что это действительно проверка модели, а не так же, как Java Path Finder для Java. Im i worng? Может ли он использоваться как JPF?

Мне нужно знать, была ли определенная часть кода сконфигурирована таким образом, чтобы она могла зайти в тупик. Скажем, это школьная штука, и даже если я уверен, что мой код работает, я должен ее проверить. (Да, нам разрешено и рекомендуется смотреть в Интернете).

Answer 1

Как сказал пользователь @HighCore, и после многократного поиска я могу сказать, что зрелый и современный инструмент, подобный описанному мной, не существует.

Answer 2

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

Для полного языка Turing проблема проверки неразрешима, поэтому инструменты проверки модели обычно принимают менее мощный язык в качестве входных данных, что подразумевает необходимость преобразования вашей проблемы на этот язык перед проверкой. Именно по этой причине вы не сталкивались с каким-либо «инструментом проверки модели C#».

Вы посмотрели Boogie и C#-like Dafny? Это по существу для аннотации с Hoare logic.

В качестве альтернативы вы можете рассмотреть модель, проверяющую ваше решение C# после (вручную), переведя его на Promela, а затем используя SPIN.

Связанные инструменты (например, C-> Promela translators) указаны в here.