Programming language specification and implementation

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

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.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Modeling. : 8th International Symposium, ISoLA 2018 Limassol, Cyprus, November 5–9, 2018 Proceedings, Part I
EditorsTiziana Margaria, Bernhard Steffen
Number of pages22
PublisherSpringer
Publication date2018
Pages162-183
ISBN (Print)978-3-030-03417-7
ISBN (Electronic)978-3-030-03418-4
DOIs
Publication statusPublished - 2018
SeriesLecture Notes in Computer Science
Volume11244
ISSN0302-9743

Cite this