Войти
Extended ML - это язык с широким спектром возможностей охватывает как спецификацию , так и реализацию и основывается на языке программирования ML. Он расширяет синтаксис ML, включая аксиомы , которые не обязательно должны быть исполняемыми, но могут строго определять поведение программа. Благодаря этому добавлению язык можно использовать для пошагового уточнения, постепенно переходя от начальной формальной спецификации, чтобы в конечном итоге получить исполняемую программу Standard ML. Правильность окончательной исполняемой программы SML по отношению к исходной спецификации затем может быть установлена путем доказательства правильности каждого из этапов уточнения. Расширенный ML используется для исследования и обучения формальной разработке программ и спецификации, а исследования в области автоматической проверки программ.
Расширенный ML не имеет отношения к языку программирования ( кроме аналогичных производных от ML), ни языка спецификаций eXtensible Markup Language.
.
