A Formal Semantics for Javalette in the K framework

Publicerad

Typ

Examensarbete för masterexamen

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

Index

item.page.endorsement

item.page.review

item.page.supplemented

item.page.referenced