Towards Verification of C Programs. C-Light Language and Its Formal Semantics

摘要

The C-light language is described, which is a representative subset of C. C-light permits deterministic expressions, limited use of switch and goto statements, and, instead of library functions for work with dynamic memory, includes C++ statements new and delete. A survey of structured operational semantics of the C-light language in Plotkin's style is given.