Существует ли программное обеспечение для проверки моделей (например, Java Path Finder), но для C#?
< EDIT > Об этом вопросе не по теме и слишком основанном на мнении, я постараюсь быть более ясным. Моя цель состояла в том, чтобы понять, существует ли такой инструмент, меня не интересовали мнения о том, что является лучшим. В то время, когда я писал этот вопрос, я потратил довольно много времени на поиск в интернете и нашел только старые мертвые проекты, но такой инструмент для Java существовал, и я не мог поверить, что для C# ничего не было. Я думаю, что этот вопрос связан с программированием (проверкой кода), и на самом деле это не вопрос мнения. Кроме того, найти эту информацию по-прежнему нелегко, и я думаю, что мой ответ поможет сэкономить время. Тем не менее, я не эксперт в stackru, если вы все еще думаете, что вопрос / ответ не подходит сайту, не стесняйтесь удалить его. < / EDIT >
Я нашел Moonwalker http://fmt.cs.utwente.nl/tools/moonwalker/ но последнее обновление было сделано в 2009 году, и я не думаю, что он поддерживает.net4.5 (и он плохо документирован).
Ответом на этот вопрос является предложение CodeContracts в качестве инструмента проверки моделей. Инструмент проверки моделей C#, но я пытался его использовать, и я не думаю, что это действительно средство проверки моделей, а не Java Path Finder для Java. Я, что, я работаю? Можно ли использовать как JPF?
Мне нужно знать, разработана ли определенная часть кода таким образом, чтобы она могла зайти в тупик. Допустим, это школьная вещь, и даже если я уверен, что мой код работает, я должен проверить его на модели. (Да, нам разрешено и рекомендуется смотреть в Интернете).
2 ответа
Как сказал пользователь @HighCore, и после долгих поисков могу сказать, что зрелого и современного инструмента, подобного тому, который я описал, не существует.
Проверка модели обычно относится к явным методам, однако символические методы в равной степени продвинуты и, возможно, более способны устанавливать свойства реального кода.
Для полного языка Тьюринга проблема проверки неразрешима, поэтому инструменты проверки моделей обычно принимают в качестве входных данных менее мощный язык, что подразумевает необходимость преобразования вашей проблемы в этот язык перед проверкой. Это причина того, что вы не сталкивались с каким-либо "инструментом проверки модели C#".
Вы смотрели на Буги и Дафни в стиле C#? Это по существу для аннотирования с логикой Хоара.
В качестве альтернативы, вы можете рассмотреть проверку модели вашего решения C# после (вручную) перевода его в Promela, а затем с помощью SPIN.
Связанные инструменты (например, C-> Promela переводчики) перечислены здесь.