Comments on Always-true is not invariant: Assertional reasoning about invariance

DOI10.1016/0020-0190(91)90115-XzbMath0743.68094MaRDI QIDQ1183477

Jimmi S. Pettersson

Publication date: 28 June 1992

Published in: Information Processing Letters (Search for Journal in Brave)

zbMATH Keywords

invarianceprogram compositionprogram correctnessassertional reasoning

Mathematics Subject Classification ID

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

Related Items

Invariants, composition, and substitution ⋮ Automatic Verification of Bossa Scheduler Properties

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Eliminating the substitution axiom from UNITY logic
• Comments on ``On the proof of a distributed algorithm: Always-true is not invariant