MURAL - Maynooth University Research Archive Library



    Tactics for Transformational Programming


    Monahan, Rosemary and Geiselbrechtinger, Franz (1997) Tactics for Transformational Programming. In: 1st Irish Workshop on Formal Methods, July 3-4, 1997, Trinity College Dublin.

    [img]
    Preview
    Download (83kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

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

    Item Type: Conference or Workshop Item (Paper)
    Keywords: Transformational Programming; Formal Methods; theorem proving;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 8251
    Depositing User: Rosemary Monahan
    Date Deposited: 29 May 2017 15:30
    Refereed: Yes
    URI:

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year