The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

MSc Thesis #9596

Title:Using Mollusc to Guide Raise Proofs
Date: 1995
Abstract:RAISE ("Rigorous Approach to Industrial Software Engineering") is a formal method for specifying and developing large software systems. it contains a proof tool, the RAISE Justification Editor, or JE. To prove by JE makes proofs hard to construct because it requires the user to reason at a very low level. In practice it becomes very difficult to use for large-scale proof. There is no abstraction mechanism from the detail of the proof process, so that a proof must be presented to the editor as a very long sequence of applications of elementary proof rules. Up to this moment, there is no way of composing such sequences into any larger entities such as tactics. The proof checker Mollusc is an interactive proof development shell which can be ;used to construct and edit proofs in any sequent-based logic [Richards et al. 94]. Thus, we will import the RAISE logic into Mollusc. Tactics could subsequently be used to provide higher-level interaction. This project will focus on how to build the RAISE logic with a side-condition "assignment-disjoint" linking together common sequences of rule applications. We discuss how it can help to speed-up and simplify the proof process.

[Search These Pages] [DAI Home Page] [Comment]