Why3
От: Эйнсток Файр Мухосранск https://raw.githubusercontent.com/EinstokFair/notes-in-russian-language/gh-pages/images/ugroza.gif
Дата: 09.08.21 21:01
Оценка:
Расскажите, пожалуйста, про Why3 (ну, в смысле, хотели бы вы его использовать в вашем идеальном проекте или нет)

Formalising the semantics of programming language is most of the time done using interactive proof assistants like Coq or Isabelle. Yet, formalising semantics and proving complex properties, with automatic provers only, was already shown possible by Clochard et. al, who also use the Why3 environment.

why3 coq isabelle доказательство
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.