University of Limerick
Browse
Butterfield-Saoithin.pdf (1.76 MB)

Saoithin : a theorem prover for UTP

Download (1.76 MB)
conference contribution
posted on 2011-02-02, 20:55 authored by Andrew Butterfield
Saoithin is a theorem prover developed to support the Unifying Theories of Programming (UTP) framework. Its primary design goal was to support the higher-order logic, alphabets, equational reasoning and "programs as predicates" style that is prevalent in much of the UTP literature, from the seminal work by Hoare & He [HH98] onwards. This paper describes the key features of the theorem prover, with an emphasis on the underlying foundations, and how these affect the design and implementation choices. These key features include: a formalisation of a UTP Theory; support for common proof strategies; sophisticated goal/law matching ; and user-de ned language constructs. A simple theory of designs with some proof extracts is used to illustrate the above features. The theorem prover has been used with undergraduate students and we discuss some of those experiences. The paper then concludes with a discussion of current limitations and planned improvements to the tool.

History

Publication

Unifying Theories of Programming;6445,2010/ pp. 137-156

Publisher

Springer-Verlag

Note

peer-reviewed

Other Funding information

SFI

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC