Programmirung
The paper presents the language C-light which is representative ve-ri-fi-cation-oriented subset of standard C. This language allows deterministic expressions and limited use of statements switch and goto. C-light includes C$++$ operators new and delete to manage dynamic memory instead of standard C library functions. The full structural operational semantics of C-light in the style of Plotkin is presented. The use of C-light as an input language of program verification system is intended.
Full Text in Russian: | HTML |
Comments |
[Home] [Conference] |
©2001, Siberian Branch of Russian Academy of Science, Novosibirsk
©2001, United Institute of Computer Science SB RAS, Novosibirsk
©2001, Institute of Computational Techologies SB RAS, Novosibirsk
©2001, A.P. Ershov Institute of Informatics Systems SB RAS, Novosibirsk
©2001, Institute of Mathematics SB RAS, Novosibirsk
©2001, Institute of Cytology and Genetics SB RAS, Novosibirsk
©2001, Institute of Computational Mathematics and Mathematical Geophysics SB RAS, Novosibirsk
©2001, Novosibirsk State University
Last modified 06-Jul-2012 (11:45:21)