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

    Keywords

    • Programming language specification
    • Semantics and implementation
    • Functional languages
    • Formal specification
    • Nondeterminism

    Fingerprint

    Dive into the research topics of 'Programming language specification and implementation'. Together they form a unique fingerprint.

    Cite this