Rozszerzony ML

Extended ML to język o szerokim spektrum oparty na ML , obejmujący zarówno specyfikację , jak i implementację. Rozszerza składnię ML o aksjomaty , które nie muszą być wykonywalne, ale mogą rygorystycznie określać zachowanie programu. Dzięki temu dodatkowi język może być używany do stopniowego udoskonalania, postępując stopniowo od wstępnej formalnej specyfikacji , aby ostatecznie uzyskać wykonywalny standardowy program ML . Poprawność końcowego pliku wykonywalnego w odniesieniu do oryginalnej specyfikacji można następnie ustalić, udowadniając poprawność każdego z etapów udoskonalania. Extended ML jest używany do badań i nauczania formalnego tworzenia i specyfikacji programów oraz do badań nad automatyczną weryfikacją programów .

Extended ML nie jest powiązany z językiem programowania Extensible ML (poza tym, że jest podobnie wywodzący się z ML), ani z językiem specyfikacji Extensible Markup Language (XML).

• S. Kahrs, D. Sannella i A. Tarlecki. Definicja rozszerzonego ML: Delikatne wprowadzenie. Informatyka teoretyczna , 173 (2): 445–484, 28 lutego 1997 r.

Linki zewnętrzne

• Don Sannella — Informacje o rozszerzonej ML