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.
|Publication status||Published - 2002|
|Event||Computer Science and Engineering PhD Day May 2002 - |
Duration: 1 Jan 2002 → …
|Conference||Computer Science and Engineering PhD Day May 2002|
|Period||01/01/2002 → …|
Bibliographical notepp. 45-62
- proof support