Validating Formal Semantics by Property-Based Cross-Testing
Péter Bereczky, Dániel Horpácsi, Judit Köszegi, Soma Szeier, Simon Thompson
Abstract
Open-access reader
Péter Bereczky, Dániel Horpácsi, Judit Köszegi, Soma Szeier, Simon Thompson
Abstract
Open-access reader
To describe the behaviour of programs in a programming language we can define a formal semantics for the language, and formalise it in a proof assistant. From this semantics we can derive the behaviour of each particular program in the language. But there remains the question of validating the formal semantics: have we got the formalisation right?
OpenAlex reports 5 citations for this work. Citation counts describe recorded attention and do not establish research quality.
A contribution statement is not available in the OpenAlex record.
Method details are not available in the OpenAlex metadata.
Findings are not separately available in the OpenAlex metadata.
Limitations are not available in the OpenAlex metadata.
Application details are not available in the OpenAlex metadata.
To describe the behaviour of programs in a programming language we can define a formal semantics for the language, and formalise it in a proof assistant. From this semantics we can derive the behaviour of each particular program in the language. But there remains the question of validating the formal semantics: have we got the formalisation right?
Key concepts: Computer science, Programming language, Operational semantics, Formal semantics (linguistics), Semantics (computer science), Action semantics, Denotational semantics, Computational semantics