ITU

Programming language specification and implementation

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Standard

Programming language specification and implementation. / Sestoft, Peter.

Leveraging Applications of Formal Methods, Verification and Validation. Modeling.: 8th International Symposium, ISoLA 2018 Limassol, Cyprus, November 5–9, 2018 Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. Springer, 2018. p. 162-183 (Lecture Notes in Computer Science, Vol. 11244).

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Harvard

Sestoft, P 2018, Programming language specification and implementation. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Modeling.: 8th International Symposium, ISoLA 2018 Limassol, Cyprus, November 5–9, 2018 Proceedings, Part I. Springer, Lecture Notes in Computer Science, vol. 11244, pp. 162-183. https://doi.org/10.1007/978-3-030-03418-4_11

APA

Sestoft, P. (2018). Programming language specification and implementation. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Modeling.: 8th International Symposium, ISoLA 2018 Limassol, Cyprus, November 5–9, 2018 Proceedings, Part I (pp. 162-183). Springer. Lecture Notes in Computer Science Vol. 11244 https://doi.org/10.1007/978-3-030-03418-4_11

Vancouver

Sestoft P. Programming language specification and implementation. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Modeling.: 8th International Symposium, ISoLA 2018 Limassol, Cyprus, November 5–9, 2018 Proceedings, Part I. Springer. 2018. p. 162-183. (Lecture Notes in Computer Science, Vol. 11244). https://doi.org/10.1007/978-3-030-03418-4_11

Author

Sestoft, Peter. / Programming language specification and implementation. Leveraging Applications of Formal Methods, Verification and Validation. Modeling.: 8th International Symposium, ISoLA 2018 Limassol, Cyprus, November 5–9, 2018 Proceedings, Part I. editor / Tiziana Margaria ; Bernhard Steffen. Springer, 2018. pp. 162-183 (Lecture Notes in Computer Science, Vol. 11244).

Bibtex

@inproceedings{1fe22cdf8f0845f0816d671da37ed604,
title = "Programming language specification and implementation",
abstract = "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.",
author = "Peter Sestoft",
year = "2018",
doi = "10.1007/978-3-030-03418-4_11",
language = "English",
isbn = "978-3-030-03417-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "162--183",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Modeling.",
address = "Germany",

}

RIS

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.

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 -

ID: 83565749