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

Preview

Download (83kB) | Preview

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:	http://ewic.bcs.org/category/17095
Use Licence:	This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

Repository Staff Only(login required)

Item control page

Downloads

Origin of downloads