Derivation of Invariant Assertions During Program Development by Transformation

DOI10.1145/357103.357108zbMath0468.68016OpenAlexW2059976750MaRDI QIDQ3922137

Bernd Krieg-Brückner, Manfred Broy

Publication date: 1980

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/357103.357108

zbMATH Keywords

verificationiterationinvariantscorrectnessrecursionprogram transformationsspecificationassertionsrecursion removal

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (3)

Running programs backwards: The logical inversion of imperative computation ⋮ SPECIFICATION AND COMPUTING STATES IN FUZZY ALGORITHMS ⋮ Definite Descriptions and Dijkstra's Odd Powers of Odd Integers Problem

This page was built for publication: Derivation of Invariant Assertions During Program Development by Transformation