A Formal Semantics for Javalette in the K framework

dc.contributor.authorBurak Bilge, Yalcinkaya
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.contributor.examinerAbel, Andreas
dc.contributor.supervisorMyreen, Magnus
dc.date.accessioned2022-09-15T10:02:58Z
dc.date.available2022-09-15T10:02:58Z
dc.date.issued2022sv
dc.date.submitted2020
dc.description.abstractThis 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.sv
dc.identifier.coursecodeDATX05sv
dc.identifier.urihttps://hdl.handle.net/20.500.12380/305603
dc.language.isoengsv
dc.setspec.uppsokTechnology
dc.subjectFormal semanticssv
dc.subjectK frameworksv
dc.subjectprogramming languagessv
dc.subjectJavalettesv
dc.titleA Formal Semantics for Javalette in the K frameworksv
dc.type.degreeExamensarbete för masterexamensv
dc.type.uppsokH
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Hämtar...
Bild (thumbnail)
Namn:
CSE 22-28 Yalcinkaya.pdf
Storlek:
1.37 MB
Format:
Adobe Portable Document Format
Beskrivning:
A Formal Semantics for Javalette in the K framework
License bundle
Visar 1 - 1 av 1
Hämtar...
Bild (thumbnail)
Namn:
license.txt
Storlek:
1.51 KB
Format:
Item-specific license agreed upon to submission
Beskrivning: