A Formal Semantics for Javalette in the K framework

Typ
Examensarbete för masterexamen
Program
Publicerad
2022
Författare
Burak Bilge, Yalcinkaya
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
This thesis is about developing an executable formal semantics for Javalette in the K framework. Javalette is an imperative programming language. Its syntax is formally specified using BNF (Backus-Naur form) notation, but it does not have a formal semantics. The semantics of the language is informally documented in English. Javalette has several extensions that enrich the language’s syntax and semantics with new types, statements, and expressions. K is a toolset for programming language design and implementation. It provides a specification language for formally defining syntax and semantics. From these definitions, K automatically generates various tools such as parsers, interpreters, model checkers, and deductive verifiers. The purpose of this project is to develop a complete formal semantics for the Javalette language, design an architecture for extending the language modularly and implement language extensions, find and resolve undefined behaviors in the language, and use the formal semantics to develop an input fuzzer for testing Javalette programs and implementations.
Beskrivning
Ämne/nyckelord
Formal semantics, K framework, programming languages, Javalette
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material