Specify in RSL and Prove in Isabelle | Morten P. Lindegaard
| | Abstract | An approach to increasing proof support for the RAISE method is to translate RSL specifications to Isabelle/HOL and use the theorem prover Isabelle. Institutions and institution representations are used as foundations for the translation. To describe the model-theoretic semantics of RSL, the concept of looser semantics is introduced. An institution for a subset of RSL is presented, higher-order logic is considered, and it is outlined how to translate RSL specifications into Isabelle/HOL. | | Keywords | RSL, Isabelle, HOL, RAISE, proof support, institutions. | | Type | Misc [Presentation] | | Journal/Book/Conference | Computer Science and Engineering PhD Day May 2002 | | Year | 2002 Month May pp. 45-62 | | Publisher | IMM, Technical University of Denmark | | Address | DTU, DK-2800 Kgs. Lyngby | | IMM no. | IMM-TR-2002-8 | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|