Calculation of Invariants Assertions
In this paper we present a series of theorems that allow to establish strategies for the calculation of invariant assertions, such as the Dijkstra’s Hk(Post), or the weakest precondition of the loop. A criterion is also shown for calculating the termination condition of a loop. As in the integrals c...
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Objeto de conferencia |
| Lenguaje: | Inglés |
| Publicado: |
2017
|
| Materias: | |
| Acceso en línea: | http://sedici.unlp.edu.ar/handle/10915/65163 |
| Aporte de: |
| id |
I19-R120-10915-65163 |
|---|---|
| record_format |
dspace |
| institution |
Universidad Nacional de La Plata |
| institution_str |
I-19 |
| repository_str |
R-120 |
| collection |
SEDICI (UNLP) |
| language |
Inglés |
| topic |
Ciencias Informáticas Cálculos invariant assertions formal program verification GCL induction |
| spellingShingle |
Ciencias Informáticas Cálculos invariant assertions formal program verification GCL induction Flaviani, Federico Calculation of Invariants Assertions |
| topic_facet |
Ciencias Informáticas Cálculos invariant assertions formal program verification GCL induction |
| description |
In this paper we present a series of theorems that allow to establish strategies for the calculation of invariant assertions, such as the Dijkstra’s Hk(Post), or the weakest precondition of the loop. A criterion is also shown for calculating the termination condition of a loop. As in the integrals calculus, the strategies proposed here to perform the calculation of an invariant, will depend on the shape of the loop with which it is working, particularly will work with for-type loops with or without early termination due to a sentry. |
| format |
Objeto de conferencia Objeto de conferencia |
| author |
Flaviani, Federico |
| author_facet |
Flaviani, Federico |
| author_sort |
Flaviani, Federico |
| title |
Calculation of Invariants Assertions |
| title_short |
Calculation of Invariants Assertions |
| title_full |
Calculation of Invariants Assertions |
| title_fullStr |
Calculation of Invariants Assertions |
| title_full_unstemmed |
Calculation of Invariants Assertions |
| title_sort |
calculation of invariants assertions |
| publishDate |
2017 |
| url |
http://sedici.unlp.edu.ar/handle/10915/65163 |
| work_keys_str_mv |
AT flavianifederico calculationofinvariantsassertions |
| bdutipo_str |
Repositorios |
| _version_ |
1764820480201588739 |