Link Search Menu Expand Document


Grigore Rosu gave a definition of IMP in the K framework. He wrote:

IMP is considered a folklore language, without an official inventor, and has been used in many textbooks and papers, often with slight syntactic variations and often without being called IMP. It includes the most basic imperative language constructs, namely basic constructs for arithmetic and Boolean expressions, and variable assignment, conditional, while loop and sequential composition constructs for statements.

IMP is a very small imperative language. Its CBS specification illustrates the basic features of the framework. The start of the specification of IMP in CBS is at IMP.



  • abstract syntax: complete, derived from IMP in the K framework
  • dynamic semantics: complete
  • static semantics: not relevant
  • disambiguation: incomplete


  • 9 tests and 3 small programs
  • high coverage (to be verified)


  • supersedes CBS of IMP in all previously published papers

Reuse of funcons:



  • imperative, illustrative, simple, disambiguation, K framework

Main contributors:

  • Peter Mosses

Table of contents