Hoare Logic and Auxiliary Variables
|
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
|
|
|
Hoare Logic and Auxiliary Variables
|
| Id. |
46320583 |
| Idioma |
inglés
|
| Titulo |
Hoare Logic and Auxiliary Variables |
| Autor(es) |
Thomas Kleymann
|
| Localización |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.9009
|
| Versión |
1.0 |
| Estado |
Final
|
| Descripción |
Auxiliary variables are essential for specifying programs in Hoare Logic. They are required to relate the value of variables in different states. However, the axioms and rules of Hoare Logic turn a blind eye to the rle of auxiliary variables. We stipulate a new structural rule for adjusting auxiliary variables when strengthening preconditions and weakening postconditions. Courtesy of this new rule, Hoare Logic is adaptation complete, which benefits software re-use. This property is responsible for a number of improvements. Relative completeness follows uniformly from the Most General Formula property. Moreover, contrary to common belief, one can show that Hoare Logic subsumes VDM's operation decomposition rules in that every derivation in VDM can be naturally embedded in Hoare Logic. Furthermore, the new treatment leads to a significant simplification in the presentation for verification calculi dealing with more interesting features such as recursion or concurrency.
|
| Tipo |
application/postscript
|
| Palabras clave |
Hoare Logic
|
| 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/postscript
|
| Requerimientos técnicos |
Browser: Any
|
| Relación |
[IsBasedOn] http://www.lfcs.informatics.ed.ac.uk/reports/98/ECS-LFCS-98-399/ECS-LFCS-98-399.ps.gz
[References] 10.1.1.116.2392
[References] 10.1.1.130.1486
[References] 10.1.1.59.3430
[References] 10.1.1.65.4684
[References] 10.1.1.92.7181
[References] 10.1.1.43.2254
[References] 10.1.1.113.7280
[References] 10.1.1.124.9532
[References] 10.1.1.111.2692
[References] 10.1.1.66.9439
[References] 10.1.1.28.4813
[References] 10.1.1.110.7127
[References] 10.1.1.28.8243
[References] 10.1.1.105.5495
[References] 10.1.1.22.8547
[References] 10.1.1.25.7898
[References] 10.1.1.62.6175
[References] 10.1.1.105.9489
[References] 10.1.1.88.7589
[References] 10.1.1.96.2342
[References] 10.1.1.118.7567
[References] 10.1.1.119.7063
[References] 10.1.1.123.6334
|
| Fecha de contribución |
24-jul-2009 |
| Contacto |
|
|
|
|
|
Valoración de los usuarios
No hay ninguna valoración para este recurso. Sea el primero en
valorar este recurso.
|
|
|
|
