Extended ML

Extended ML é un linguaxe de programación creado por Kahrs, Sannella e Tarlecki baseado en ML. Estende a sintaxe de ML para incluír axiomas de semántica, os cales poden non ser executables pero que serven para especificar rigorosamente o comportamento dun programa. Con esta extensión a linguaxe pode utilizarse para aplicar técnicas de refinamiento de programas para, a partir dunha especificación formal, producir un programa na linguaxe Standard ML que cumpre coa especificación. Extended ML utilízase para o ensino de desenvolvemento formal de programas, especificación de programas e para investigación en verificación automatizada de programas.

Ligazóns externas

• Don Sannella - Información sobre Extended ML

Notas

• S. Kahrs, D. Sannella, e A. Tarlecki. The definition of extended ML: A gentle introduction. Theoretical Computer Science, 173(2):445-484, 28 Feb 1997.