Weakest preconditions for progress

DOI10.1007/BF01212336MaRDI QIDQ1189258zbMATH OpenOpenAlexFDO

Authors Johan J. Lukkien, Jan L. A. van de Snepscheut

Publication date 26 September 1992

Published in Formal Aspects of Computing (Search for Journal in Brave)

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

zbMATH Keywords

progress propertiesweakest preconditions

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

The authors begin their study with an overview of results on predicates and predicate transformers as used in this context. It provides the notation and terminology for the remainder of this paper. Next, they link a predicate transfer for expressing progress properties to an operational interpretation of program execution. This leads to a set of requirements that seem reasonable to expect from any predicate transformer that satisfies the interpretation. The authors define the predicate transformer by induction over the program structure, and they establish some theorems about it. Finally, they repeat these steps for another progress property and its predicate transformer.

Recommendations

• A predicate transformer for progress
• A predicate transformer for the progress property `to-always'
• scientific article; zbMATH DE number 1531358
• Weakest precondition semantics for time and concurrency
• Safety and progress of recursive procedures

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Proving Liveness Properties of Concurrent Programs
• Temporal predicate transformers and fair termination

Cited in

(5)

• Safety and progress of recursive procedures
• Properties of a predicate transformer of the VRS system
• Weakest preconditions for pure Prolog programs
• scientific article; zbMATH DE number 1531358 (Why is no real title available?)
• A predicate transformer for progress

Describes a project that uses

Uses Software

• UNITY

This page was built for publication: Weakest preconditions for progress

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1189258)