Text size
  • Small
  • Medium
  • Large
  • Standard
  • Blue text on blue
  • High contrast (Yellow text on black)
  • Blue text on beige

    Declarative View of Imperative Programs

    2nd Irish Workshop on Formal Methods

    Cork, Ireland. 2nd - 3rd July 1998


    H. Gibbons


    By giving a declarative meaning to an imperative program, the verification of the imperative program is switched from the imperative paradigm to the declarative or logic paradigm where one can take advantage of, for example, referential transparency.

    Rather than 'compiling' an imperative program to a 'lower level' we 'inverse compile' the imperative program to the 'higher' declarative level.

    The declarative view of an imperative program is a predicate associated with the imperative program such that if this predicate satisfies the specification of the program then the imperative program is correct relative to the specification.

    In one sense the associated predicate gives a declarative meaning to the imperative program.


    PDF filePDF Version of this Paper (82kb)