A Formal Semantics for Javalette in the K framework
Ladda ner
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