Skip to main content

Is Sometimes Ever Better Than Alway?

DOI 10.1145/357073.357080 dblp BibTeX

Abstract

The “intermittent assertion” method for proving programs correct is explained and compared with the conventional method. Simple conventional proofs of iterative algorithms that compute recursively defined functions, including Ackermann's function, are given.

Related papers

"Sometime" is Sometimes "Not Never" - On the Temporal Logic of Programs POPL 1980
Optimizing N-dimensional, winograd-based convolution for manycore CPUs PPoPP 2018
Pantaxou: a domain-specific language for developing safe coordination services GPCE 2008
Pretenuring for Java OOPSLA 2001
A hierarchy of mendler style recursion combinators: taming inductive datatypes with negative occurrences ICFP 2011
Implementation of an Array Bound Checker POPL 1977
More than you ever wanted to know about synchronization: synchrobench, measuring the impact of the synchronization on concurrent algorithms PPoPP 2015
Efficiently Learning Locality Optimizations by Decomposing Transformation Domains CC 2023