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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Flaviani, Federico
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 2017
Materias:
GCL
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