TY - GEN
T1 - Programming language specification and implementation
AU - Sestoft, Peter
PY - 2018
Y1 - 2018
N2 - The specification of a programming language is a special case of the specification of software in general. This paper discusses the relation between semantics and implementation, or specification and program, using two very different languages for illustration. First, we consider small fragments of a specification of preliminary Ada, and show that what was considered a specification in VDM in 1980 now looks much like an implementation in a functional language. Also, we discuss how a formal specification may be valuable even though seen from a purely formal point of view it is flawed. Second, we consider the simple language of spreadsheet formulas and give a complete specification. We show that nondeterminism in the specification may reflect run-time nondeterminism, but also underspecification, that is, implementation-time design choices. Although specification nondeterminism may appear at different binding-times there is no conventional way to distinguish these. We also consider a cost semantics and find that the specification may need to contain some “artificial” nondeterminism for underspecification.
AB - The specification of a programming language is a special case of the specification of software in general. This paper discusses the relation between semantics and implementation, or specification and program, using two very different languages for illustration. First, we consider small fragments of a specification of preliminary Ada, and show that what was considered a specification in VDM in 1980 now looks much like an implementation in a functional language. Also, we discuss how a formal specification may be valuable even though seen from a purely formal point of view it is flawed. Second, we consider the simple language of spreadsheet formulas and give a complete specification. We show that nondeterminism in the specification may reflect run-time nondeterminism, but also underspecification, that is, implementation-time design choices. Although specification nondeterminism may appear at different binding-times there is no conventional way to distinguish these. We also consider a cost semantics and find that the specification may need to contain some “artificial” nondeterminism for underspecification.
KW - Programming language specification
KW - Semantics and implementation
KW - Functional languages
KW - Formal specification
KW - Nondeterminism
KW - Programming language specification
KW - Semantics and implementation
KW - Functional languages
KW - Formal specification
KW - Nondeterminism
U2 - 10.1007/978-3-030-03418-4_11
DO - 10.1007/978-3-030-03418-4_11
M3 - Article in proceedings
SN - 978-3-030-03417-7
T3 - Lecture Notes in Computer Science
SP - 162
EP - 183
BT - Leveraging Applications of Formal Methods, Verification and Validation. Modeling.
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer
ER -