Abstract
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 switch and goto. C-light includes the C++ operators new and delete to manage the dynamic memory instead of standard C library functions. The structural operational semantics of C-light in the Plotkin style is outlined. © Springer-Verlag Berlin Heidelberg 2003.
Cite
CITATION STYLE
Nepomniaschy, V. A., Anureev, I. S., & Promsky, A. V. (2003). Verification-oriented language C-light and its structural operational semantics. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2890, 103–111. https://doi.org/10.1007/978-3-540-39866-0_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
