Advertisement

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

  • Valery A. Nepomniaschy
  • Igor S. Anureev
  • Alexey V. Promsky
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)

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 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Apt, K.R., Olderog, E.R.: Verification of sequential and concurrent programs. Springer, Berlin (1991)zbMATHGoogle Scholar
  2. 2.
    Gurevich, Y., Huggins, J.K.: The semantics of the C programming language. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 274–309. Springer, Heidelberg (1993)Google Scholar
  3. 3.
    Huggins, J.K., Shen, W.: The static and dynamic semantics of C (extended abstract). In: Local Proc. Int. Workshop on Abstract State Machines, Zurich, pp. 272–284 (2000) (ETH TIK-Rep.; N 87)Google Scholar
  4. 4.
    ISO/IEC 9899:1999, Programming languages — C (1999)Google Scholar
  5. 5.
    Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. The language C-light and its formal semantics. — Programmirovanie (6), 1–13 (2002) (in Russian)Google Scholar
  6. 6.
    Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. Part 1. Language C-light. — A.P. Ershov Institute of Informatics Systems, Report N 84. — Novosibirsk (2001) (in Russian)Google Scholar
  7. 7.
    Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. Part 2. Language C-light-kernel and its axiomatic semantics. — A.P. Ershov Institute of Informatics Systems, Report N 87. — Novosibirsk (2001) (in Russian)Google Scholar
  8. 8.
    Nepomniaschy, V.A., Anureev, I.S., Michailov, I.N., Promsky, A.V.: Towards C program verificaton. Part 3. Translation from C-light into C-light-kernel and its formal justification. A.P. Ershov Institute of Informatics Systems, Report N 97. — Novosibirsk (2002) (in Russian)Google Scholar
  9. 9.
    Norrish, M.: Deterministic expressions in C. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 147–161. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Norrish, M.: C formalised in HOL.— PhD thesis, Computer Lab., Univ of Cambridge (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Valery A. Nepomniaschy
    • 1
  • Igor S. Anureev
    • 1
  • Alexey V. Promsky
    • 1
  1. 1.Siberian Division of the Russian Academy of SciencesA. P. Ershov Institute of Informatics SystemsNovosibirskRussia

Personalised recommendations