Problem-oriented program verification
We describe a methodology of problem-oriented program verification which includes a special invariant-free derivation rule for a loop writing into a file, an identity condition for sequential and parallel replacement in arrays, which simplifies the proof of correctness conditions, and also a transformation to remove the goto statement from the body of a loop.
sequential and parallel replacement in arrays
scientific article; zbMATH DE number 3972171