Constructor-based Observational Logic ⋆
|
Descargar SCORM
Este recurso ha sido solicitado 1 veces (0 veces en los últimos 31 días).
Para poder solicitar este recurso debe identificarse como usuario de la biblioteca
|
| |
Ver
Detalles del recurso
|
|
|
Constructor-based Observational Logic ⋆
|
| Id. |
47353060 |
| Idioma |
inglés
|
| Titulo |
Constructor-based Observational Logic ⋆ |
| Autor(es) |
Observational Logic
Michel Bidoit A
Rolf Hennicker B
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.78.5940
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
This paper focuses on the integration of reachability and observability concepts within an algebraic, institution-based framework. In the first part of this work, we develop the essential ingredients that are needed to define the constructorbased observational logic institution, called COL, which takes into account both the generation- and observation-oriented aspects of software systems. The underlying paradigm of our approach is that the semantics of a specification should be as loose as possible to capture all its correct realizations. We also consider the “black box ” semantics of a specification which is useful to study the behavioral properties a user can observe when he/she is experimenting with the system. In the second part of this work, we develop proof techniques for structured COLspecifications. For this purpose we introduce an institution encoding from the COL institution to the usual institution of many-sorted first-order logic with equality and sort-generation constraints. Using this institution encoding, we can then reduce proofs of consequences of structured specifications built over COL to proofs of consequences of structured specifications written in a simple subset of the algebraic specification language Casl. This means, in particular, that any inductive theorem prover, such as e.g. Larch or PVS, can be used to prove theorems over structured COL-specifications.
|
| Tipo |
application/pdf
|
| Palabras clave |
URLs
|
| Tipo de recurso |
Texto Narrativo
|
| Tipo de Interactividad |
Expositivo
|
| Nivel de Interactividad |
muy bajo
|
| Audiencia |
Estudiante
Profesor
Autor
|
| Estructura |
Atomic |
| Coste |
no
|
| Copyright |
sí
|
|
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| Formatos |
application/pdf
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://www.lsv.ens-cachan.fr/~bidoit/rr-lsv-2003-9.rr.pdf
[References] 10.1.1.137.5123
[References] 10.1.1.70.5436
[References] 10.1.1.13.3624
[References] 10.1.1.16.1071
[References] 10.1.1.34.1552
[References] 10.1.1.26.260
[References] 10.1.1.34.4434
[References] 10.1.1.17.8745
[References] 10.1.1.23.1808
[References] 10.1.1.48.5474
[References] 10.1.1.27.6963
[References] 10.1.1.128.1181
[References] 10.1.1.117.1458
[References] 10.1.1.37.36
[References] 10.1.1.25.9628
[References] 10.1.1.16.1572
[References] 10.1.1.13.5903
|
| Fecha de contribución |
01-sep-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
