Programming language specification and implementation

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review


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.
TitelLeveraging Applications of Formal Methods, Verification and Validation. Modeling. : 8th International Symposium, ISoLA 2018 Limassol, Cyprus, November 5–9, 2018 Proceedings, Part I
RedaktørerTiziana Margaria, Bernhard Steffen
Antal sider22
ISBN (Trykt)978-3-030-03417-7
ISBN (Elektronisk)978-3-030-03418-4
StatusUdgivet - 2018
NavnLecture Notes in Computer Science


Dyk ned i forskningsemnerne om 'Programming language specification and implementation'. Sammen danner de et unikt fingeraftryk.