The trouble with for-loop invariants

In this paper we discuss some of the problems in constructing and utilizing loop invariants for For-loops. Another kind of assertion, the loop post-invariant, is offered as an alternative to the loop invariant in designing, documenting and proving the correctness of For-loops.

Saved in:
Bibliographic Details
Main Author: Collins, William J.
Format: Conference Proceeding
Language:English
Subjects:
Software and its engineering > Software organization and properties > Software functional properties > Correctness
Theory of computation > Logic > Proof theory
Theory of computation > Semantics and reasoning > Program reasoning > Invariants
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper we discuss some of the problems in constructing and utilizing loop invariants for For-loops. Another kind of assertion, the loop post-invariant, is offered as an alternative to the loop invariant in designing, documenting and proving the correctness of For-loops.
ISSN:0097-8418
DOI:10.1145/52964.52966