IMP-Start

Language "IMP"

[ #1 Arithmetic expressions
  #2 Boolean expressions
  #3 Statements and blocks
  #4 Programs and variable declarations
  #A Disambiguation
]

# Top level


Syntax
  START: start ::= pgm
Semantics
  start[[_:start]] : =>null-type

Rule

  start[[ Pgm ]] = 
    initialise-binding 
    initialise-storing 
    initialise-giving
    finalise-failing
      run[[ Pgm ]]

/*

  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 useful for a first illustration of CBS. See the CBS [Browsing Guide]
  for explanation of the meta-notation.

  [IMP in the K framework]: http://www.kframework.org/language-pdfs/new/imp.pdf 
  
  [Browsing Guide]: https://plancomps.github.io/CBS-beta/Guide/Browsing.html

*/

/* CBS-beta/Languages-beta/IMP/IMP-cbs released 2018-07-07


* Status: 
  - abstract syntax:   complete, derived from [IMP in the K framework]
  - dynamic semantics: complete
  - static semantics:  not relevant
  - disambiguation:    incomplete
* Tests:
  - 9 tests and 3 small programs
  - high coverage (to be verified)
* Evolution:
  - supersedes CBS of IMP in all previously published papers
* References:
  [IMP in the K framework]:
    http://www.kframework.org/language-pdfs/new/imp.pdf
* Keywords: 
  - imperative, illustrative, simple, disambiguation, K framework
* Main contributors:
  - recent: Peter Mosses

*/