Division of Informatics
Forrest Hill & 80 South Bridge

MSc Thesis #9596
Title:	Using Mollusc to Guide Raise Proofs
Authors:	Wu,T
Date:	1995
Presented:
Keywords:
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.
Download:	NO ONLINE COPY

Division of InformaticsForrest Hill & 80 South Bridge