NDLI: Is “sometime” sometimes better than “always”?

Content Provider	ACM Digital Library
Author	Manna, Zohar Waldinger, Richard
Abstract	This paper explores a technique for proving the correctness and termination of programs simultaneously. This approach, the intermittent-assertion method, involves documenting the program with assertions that must be true at some time when control passes through the corresponding point, but that need not be true every time. The method, introduced by Burstall, promises to provide a valuable complement to the more conventional methods.The intermittent-assertion method is presented with a number of examples of correctness and termination proofs. Some of these proofs are markedly simpler than their conventional counterparts. On the other hand, it is shown that a proof of correctness or termination by any of the conventional techniques can be rephrased directly as a proof using intermittent assertions. Finally, it is shown how the intermittent-assertion method can be applied to prove the validity of program transformations and the correctness of continuously operating programs.
Starting Page	159
Ending Page	172
Page Count	14
File Format	PDF
ISSN	00010782 15577317
DOI	10.1145/359340.359353
Journal	Communications of the ACM (CACM)
Volume Number	21
Issue Number	2
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2005-08-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Intermittent assertions Termination of programs Continuously operating programs Program transformation Correctness of programs Program verification
Content Type	Text
Resource Type	Article
Subject	Computer Science Computer Science

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Is “sometime” sometimes better than “always”?: Intermittent assertions in proving program correctness

Formal verification of parallel programs

Is Sometimes Ever Better Than Always?

A view of program verification

Test data as an aid in proving program correctness

Logical analysis of programs

On the proof of correctness of a calendar program

Sometimes, Smaller is Better. And Plenty is Better Than too Much

Parallel programs

Is “sometime” sometimes better than “always”?

Similar Documents

Is “sometime” sometimes better than “always”?: Intermittent assertions in proving program correctness

Formal verification of parallel programs

Is Sometimes Ever Better Than Always?

A view of program verification

Test data as an aid in proving program correctness

Logical analysis of programs

On the proof of correctness of a calendar program

Sometimes, Smaller is Better. And Plenty is Better Than too Much

Parallel programs

Is “sometime” sometimes better than “always”?