4 ms·
Tests are not sound in the sense of conventional program logic (overapproximation). O'Hearn's [1] even proves a soundness theorem. So when you say say [1] is
by Cladode 7y ago
Tests are not sound in the sense of conventional program logic (overapproximation). O'Hearn's [1] even proves a soundness theorem. So when you say say [1] is not sound then this is confusing for the reader.
- pron 7y ago> Tests are not sound in the sense of conventional program logic (overapproximation). Of course they are, in the logic sense of "sound", and in the same sense that incorrectness logic is sound. A test is a proof of a proposition about a single program behavior (provided that the execution is deterministic). But neither testing nor incorrectness logic are sound in the sense that term is used in software verification, namely as proofs of some explicit or implied universal proposition. In software verification, a sound technique is one that guarantees conformance to a specification over all behaviors (or conversely, the absence of spec violations in any behavior).
- Cladode 7y agoIn software verification, a sound technique is ... In other words, tests are not sound ... Anyway, we are quibbling about meaning of words, so this is unlikely to be fruitful.