| Kľúčové slová: | bezpečné programy, návrh rozhrania, príležitostné slovo, subštrukturálne typy, lineárne typy, Rust, C++, Haskell
|
|---|
| Abstrakt: | V práci sa zaoberáme typovou kontrolou kompilovaných jazykov, pričom skúmame možnosti typových systémov, v ktorých neplatia všetky štrukturálne pravidlá.
Podľa toho sa nazývajú subštrukturálne typové systémy, a umožňujú v zmysle typovej kontroly zachytiť niektoré dodatočné požiadavky na prácu s hodnotami.
Naša práca nadväzuje na článok \cite{ostertagLinear}, ktorý využitie subštrukturálnych typov ukazoval na príklade príležitostných slov v jazyku Rust.
Hlavnými cieľmi práce je lepšie preskúmať subštrukturálne typové systémy, a tiež iné programovacie jazyky (Rust, C++ a Haskell), ktoré poskytujú nástroje umožňujúce realizáciu týchto systémov.
Tieto nástroje nie sú vždy zavádzané so zámerom vytvorenie subštrukturálneho systému, ale ukzauje sa, že ich môžu realizovať.
Cieľom je teda zistiť, ktoré konkrétne systémy tieto jazyky dokážu realizovať, a pomocou týchto systémov definovať rozhranie pre príležitostné slovo ako príklad prvku, ktorého použitie nám umožnia vhodne kontrolovať.
Pre systémové jazyky, akými sú C++ a Rust, tiež skúmame dopad takejto kontroly na výkon programu počas behu aj na kompiláciu pri vývoji.
|
|---|