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

    Tactics for Transformational Programming

    1st Irish Workshop on Formal Methods

    Dublin, Ireland. 3rd - 4th July 1997


    R. Monahan & F. Geiselbrechtinger


    This paper discusses the relationship between transformational programming and theorem proving.

    It illustrates the use of the theorem proving environment as a basis for a program construction tool DEBATE 1 (Deduction Based Transformational Environment) which is under construction in University College Dublin.

    Using a theorem proving framework directly would require the user to be familiar with theorem proving details.

    The tool user should only be concerned with transformational programming steps and not with theorem proving activities. Therefore a layer of transformational tactics are discussed and presented.

    These tactics consist of the application of theorem proving tactics. However, they ensure that the user's only interaction with DEBATE are design decisions required within the transformational programming paradigm.

    The N Queens problem is used throughout the paper to demonstrate how the Isabelle theorem prover is adapted by a transformation tactic layer so that it may be used as a program construction tool.


    PDF filePDF Version of this Paper (107kb)