Infinite proof rules for loops

DOI10.1007/BF00286493zbMath0432.68007OpenAlexW122118864MaRDI QIDQ1138900

S. H. Smith

Publication date: 1980

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00286493

zbMATH Keywords

partial correctnessloop invariantsinductive assertionsgeneralized invariantsinfinite proof rules

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01)

Related Items (2)

The axiomatic semantics of programs based on Hoare's logic ⋮ A generalized nexttime operator in temporal logic

This page was built for publication: Infinite proof rules for loops