-
-
Notifications
You must be signed in to change notification settings - Fork 85
/
extended-ml.scroll
23 lines (19 loc) · 1.35 KB
/
extended-ml.scroll
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
import ../code/conceptPage.scroll
id extended-ml
name Extended ML
appeared 1985
tags pl
fileType text
centralPackageRepositoryCount 0
country United Kingdom
originCommunity University of Edinburgh
wikipedia https://en.wikipedia.org/wiki/Extended_ML
related standard-ml
summary Extended ML is a wide-spectrum language covering both specification and implementation and based on the ML programming language. It extends the syntax of ML to include axioms, which need not be executable but can rigorously specify the behavior of the program. With this addition the language can be used for stepwise refinement, proceeding gradually from an initial formal specification to eventually yield an executable Standard ML program. Correctness of the final executable SML program with respect to the original specification can then be established by proving the correctness of each of the refinement steps. Extended ML is used for research into and teaching of formal program development and specification, and research into automatic program verification. Extended ML is neither related to the programming language Extensible ML (other than being similarly derived from ML), nor to the specification language eXtensible Markup Language.
created 2004
backlinksCount 9
pageId 957110
revisionCount 29
dailyPageViews 4
appeared 1997
hopl https://hopl.info/showlanguage.prx?exp=1140