Расширенный ML - Extended ML
 | Тема этой статьи может не соответствовать Википедии общее руководство по известности. (Октябрь 2011 г.) (Узнайте, как и когда удалить этот шаблон сообщения) |
Расширенный ML это язык широкого спектра покрывая оба Технические характеристики и реализации и на основе Язык программирования ML. Он расширяет синтаксис ML, чтобы включить аксиомы, который не обязательно должен быть исполняемым, но может строго определять поведение программы. Благодаря этому добавлению язык можно использовать для пошагового уточнения, постепенно переходя от начального формальная спецификация чтобы в конечном итоге получить исполняемый файл Стандартный ML программа. Затем можно установить правильность окончательной исполняемой программы SML по отношению к исходной спецификации, доказав правильность каждого из этапов уточнения. Расширенный ML используется для исследования и обучения формальный разработка программ и Технические характеристики и исследования в области автоматических проверка программы.
Расширенный ML не имеет отношения к языку программирования. Расширяемый ML (кроме аналогичных производных от ML), ни язык спецификации расширяемый язык разметки.
Рекомендации
- С. Карс, Д. Саннелла и А. Тарлецкий. Определение расширенного ML: мягкое введение. Теоретическая информатика, 173 (2): 445–484, 28 февраля 1997 г.
внешняя ссылка
 | Этот язык программирования -связанная статья является заглушка. Вы можете помочь Википедии расширяя это. |