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!
cited_by
cites
container_end_page 4
container_issue
container_start_page 1
container_title
container_volume
creator Collins, William J.
description 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.
doi_str_mv 10.1145/52964.52966
format conference_proceeding
fullrecord <record><control><sourceid>proquest_acm_b</sourceid><recordid>TN_cdi_proquest_miscellaneous_31638326</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>31638326</sourcerecordid><originalsourceid>FETCH-LOGICAL-a2026-e8921ef9764c9c587c213bcfa9ee5e6d632e8bbf5e8f9eee09d0a1b4b4b6214a3</originalsourceid><addsrcrecordid>eNqNkEFLAzEUhAMqWGtP_oE9FA_C1rwkm02OUqwKBS8VvIUkfaGr203d7Orfd7f1B_gGZmD4eIch5AboAkAU9wXTUixGl2fkiipdamCFfD8nE0p1mSsB6pLMUvqgwyngJVcTMt_sMOva2Lsas5-q22Uhtnkd4yGrmm_bVrbp0jW5CLZOOPvLKXlbPW6Wz_n69ell-bDOLaNM5qg0Awy6lMJrX6jSM-DOB6sRC5RbyRkq50KBKgwVUr2lFpwYJBkIy6fk9vT30MavHlNn9lXyWNe2wdgnw0FyxZkcwPkJtH5vXIyfyQA14wzmOMPRR-zuH5hxbYWB_wJ6NFpP</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype><pqid>31638326</pqid></control><display><type>conference_proceeding</type><title>The trouble with for-loop invariants</title><source>Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)</source><creator>Collins, William J.</creator><contributor>Dershem, Herbert L.</contributor><creatorcontrib>Collins, William J. ; Dershem, Herbert L.</creatorcontrib><description>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.</description><identifier>ISSN: 0097-8418</identifier><identifier>ISBN: 089791256X</identifier><identifier>ISBN: 9780897912563</identifier><identifier>DOI: 10.1145/52964.52966</identifier><language>eng</language><publisher>New York, NY, USA: ACM</publisher><subject>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</subject><ispartof>Proceedings of the nineteenth SIGCSE technical symposium on Computer science education, 1988, p.1-4</ispartof><rights>1988 ACM</rights><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>309,310,780,784,789,790,23930,23931,25140,27925</link.rule.ids></links><search><contributor>Dershem, Herbert L.</contributor><creatorcontrib>Collins, William J.</creatorcontrib><title>The trouble with for-loop invariants</title><title>Proceedings of the nineteenth SIGCSE technical symposium on Computer science education</title><description>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.</description><subject>Software and its engineering -- Software organization and properties -- Software functional properties -- Correctness</subject><subject>Theory of computation -- Logic -- Proof theory</subject><subject>Theory of computation -- Semantics and reasoning -- Program reasoning -- Invariants</subject><issn>0097-8418</issn><isbn>089791256X</isbn><isbn>9780897912563</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>1988</creationdate><recordtype>conference_proceeding</recordtype><recordid>eNqNkEFLAzEUhAMqWGtP_oE9FA_C1rwkm02OUqwKBS8VvIUkfaGr203d7Orfd7f1B_gGZmD4eIch5AboAkAU9wXTUixGl2fkiipdamCFfD8nE0p1mSsB6pLMUvqgwyngJVcTMt_sMOva2Lsas5-q22Uhtnkd4yGrmm_bVrbp0jW5CLZOOPvLKXlbPW6Wz_n69ell-bDOLaNM5qg0Awy6lMJrX6jSM-DOB6sRC5RbyRkq50KBKgwVUr2lFpwYJBkIy6fk9vT30MavHlNn9lXyWNe2wdgnw0FyxZkcwPkJtH5vXIyfyQA14wzmOMPRR-zuH5hxbYWB_wJ6NFpP</recordid><startdate>19880201</startdate><enddate>19880201</enddate><creator>Collins, William J.</creator><general>ACM</general><scope>7SC</scope><scope>8FD</scope><scope>JQ2</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope></search><sort><creationdate>19880201</creationdate><title>The trouble with for-loop invariants</title><author>Collins, William J.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-a2026-e8921ef9764c9c587c213bcfa9ee5e6d632e8bbf5e8f9eee09d0a1b4b4b6214a3</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>1988</creationdate><topic>Software and its engineering -- Software organization and properties -- Software functional properties -- Correctness</topic><topic>Theory of computation -- Logic -- Proof theory</topic><topic>Theory of computation -- Semantics and reasoning -- Program reasoning -- Invariants</topic><toplevel>online_resources</toplevel><creatorcontrib>Collins, William J.</creatorcontrib><collection>Computer and Information Systems Abstracts</collection><collection>Technology Research Database</collection><collection>ProQuest Computer Science Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Collins, William J.</au><au>Dershem, Herbert L.</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>The trouble with for-loop invariants</atitle><btitle>Proceedings of the nineteenth SIGCSE technical symposium on Computer science education</btitle><date>1988-02-01</date><risdate>1988</risdate><spage>1</spage><epage>4</epage><pages>1-4</pages><issn>0097-8418</issn><isbn>089791256X</isbn><isbn>9780897912563</isbn><abstract>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.</abstract><cop>New York, NY, USA</cop><pub>ACM</pub><doi>10.1145/52964.52966</doi><tpages>4</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 0097-8418
ispartof Proceedings of the nineteenth SIGCSE technical symposium on Computer science education, 1988, p.1-4
issn 0097-8418
language eng
recordid cdi_proquest_miscellaneous_31638326
source Association for Computing Machinery:Jisc Collections:ACM OPEN Journals 2023-2025 (reading list)
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
title The trouble with for-loop invariants
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-07T21%3A01%3A16IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_acm_b&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=The%20trouble%20with%20for-loop%20invariants&rft.btitle=Proceedings%20of%20the%20nineteenth%20SIGCSE%20technical%20symposium%20on%20Computer%20science%20education&rft.au=Collins,%20William%20J.&rft.date=1988-02-01&rft.spage=1&rft.epage=4&rft.pages=1-4&rft.issn=0097-8418&rft.isbn=089791256X&rft.isbn_list=9780897912563&rft_id=info:doi/10.1145/52964.52966&rft_dat=%3Cproquest_acm_b%3E31638326%3C/proquest_acm_b%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-a2026-e8921ef9764c9c587c213bcfa9ee5e6d632e8bbf5e8f9eee09d0a1b4b4b6214a3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=31638326&rft_id=info:pmid/&rfr_iscdi=true