Syntactic Type Soundness in Structured Imperative Languages
Název česky | Syntaktické odvození vlastnosti "Type soundness" ve strukturovaných imperativních jazycích |
---|---|
Autoři | |
Rok publikování | 2007 |
Druh | Článek ve sborníku |
Konference | MEMICS 2007: Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science |
Fakulta / Pracoviště MU | |
Citace | |
www | MEMICS |
Obor | Informatika |
Klíčová slova | type soundness; imperative languages; language IPL |
Popis | Článek popisuje obecný způsob, jak prokázat vlastnosti "type soundness" ve strukturovaných imperativních jazycích. Tento způsob je ukázán na jednoduchém jazyku IPL. Program v tomto jazyce je množina funkcí. Abychom ukázali "type soundness", definujeme aproximativní syntaktický predikát, který staticky ověřuje korektnost funkce. Prezentovaný výsledek je vedlejší produkt vývoje kvantového jazyka LanQ, kde je využit pro prokázání vlastnosti "type soundness" tohoto jazyka. Přesto je možné tento postup použít v mnoha jiných existujících jazycích. |
Související projekty: |