CBS-beta

Beta-release of the CBS framework

CBS-beta on GitHubplancomps.github.io/CBS-beta/

IMP

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