Verification-Oriented Language C-Light and Its Structural Operational Semantics

Autor:	Alexey V. Promsky, Valery A. Nepomniaschy, Igor S. Anureev
Rok vydání:	2004
Předmět:	Action semantics Goto Computer science Programming language computer.software_genre computer Operational semantics Expression (mathematics) Style (sociolinguistics)
Zdroj:	Lecture Notes in Computer Science ISBN: 9783540208136 Ershov Memorial Conference
Popis:	The paper presents the language C-light which is a representative verification-oriented subset of the standard C. This language allows deterministic expressions and a limited use of the statements switchand goto. C-light includes the C++ operators newand deleteto manage the dynamic memory instead of standard C library functions. The structural operational semantics of C-light in the Plotkin style is outlined.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::5057a6ea775ad8e1b202ae0aa833d822 https://doi.org/10.1007/978-3-540-39866-0_12 Zobrazit plný text záznamu