A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic

DOI10.1016/0020-0190(92)90077-9zbMath0743.68093OpenAlexW2000899326WikidataQ58329983 ScholiaQ58329983MaRDI QIDQ1186571

Jan K. Pachl

Publication date: 28 June 1992

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

Full work available at URL: https://doi.org/10.1016/0020-0190(92)90077-9

zbMATH Keywords

fairnesslivenesscompletenessprogramming calculiprogram correctness

Mathematics Subject Classification ID

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

Related Items

On the logic of UNITY, Unity properties and sequences of states, some observations, Eliminating disjunctions of leads-to properties

Uses Software

• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Eliminating the substitution axiom from UNITY logic
• A predicate transformer for progress