Bakalářská práce

C++14 - mapping between the standard and a formal semantics

Tomáš Lesičko
Anotace

Formálna sémantika pre jazyk C++, vyvíjaná v K frameworku, sa skladá z pravidiel, kde každé pravidlo pokrýva malú časť C++. Zároveň existujú dokumenty pre C++, nazývané standard documents. Táto práca vysvetľuje základy formálnej sémantiky a K frameworku, skúma štruktúru štandardu C++ a popisuje implementáciu mapovania medzi štandardom a sémantikou.

Abstract

A formal semantics for C++ language is being developed in K framework. It consists of rules, where each rule covers a small segment of C++. At the same time, technical documents for C++ language called standard documents exist. This thesis explains the basics of formal semantics and K framework, examines the structure of the C++ standard documents, and describes the implementation of the mapping between the standard and the semantics.

Klíčová slova
C++ semantics text parsing text highlighting annotations coverage
Zadání práce

V současné době probíhají intenzivní práce na formalizaci sémantiky jazyka C++ v sémantickém frameworku K (ve spolupráci University of Illinois Urbana-Champaign a firmy RuntimeVerification Inc.). Cílem práce je navrhnout a implementovat pokud možno co nejvíce automatické mapování mezi touto formální sémantikou a standardem jazyka C++ (např. ISO/IEC 4882:2014, C++14). Výsledné mapování pak bude sloužit jak uživatelům nástrojů založených na výše zmíněné formální sémantice, tak i pro účely dalšího vývoje, např. pro integraci s novějšími verzemi standardu C++.

Pro tvorbu mapování bude nutné zpracovat metadata extrahovaná z formální sémantiky C++, zvolit vhodnou granularitu na úrovni textu standardu C++, a najít způsob automatického párování odpovídajících oblastí. Důležitou součástí práce bude vizualizace výsledného mapování, ze které bude dobře vidět, které části standardu jsou již pokryty formální sémantikou, a pro pokryté části umožní uživateli rychle nalézt odpovídající část sémantiky. Kromě toho bude výsledný nástroj umět počítat některé vhodné statistiky, např. pokrytí jednotlivých částí standardu.

Administrativní informace
Práce zkontrolována:
29. 7. 2020 15:00, doc. Mgr. Jan Obdržálek, PhD., učo 1552
Plný text práce
867,5 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
24. 9. 2020
Práce byla úspěšně obhájena

Vedoucí

doc. Mgr. Jan Obdržálek, PhD., učo 1552
KTP FI MU

Oponent

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Aplikovaná informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.