Upload resources

Upload your works to SEDICI to increase its visibility and improve its impact

 

Calculation of Invariants Assertions

2017
 
Document type: Objeto de conferencia

Abstract

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.

General information

Exposure date: septiembre 2017
Issue date: 2017
Document language: English
Event: Simposio Latinoamericano de Teoría Computacional (SLTC) - JAIIO 46 (Córdoba, 2017).
Origin: Sociedad Argentina de Informática e Investigación Operativa (SADIO)
xmlui.dri2xhtml.METS-1.0.item-dc-subject: Cálculos ; invariant assertions ; formal program verification ; GCL ; induction
Subjects: Ciencias Informáticas

Download Files

Thumbnail
Documento completo
Download file (243.0Kb) - PDF
 
Created: 26 de febrero de 2018
Available since: 26 de febrero de 2018
Please, use one of this identificators(URI) for cite o linking this item:
  • http://sedici.unlp.edu.ar/handle/10915/65163

    • This item appears in the following Collection(s)

    Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) Except where otherwise noted, this item's license is described as Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)