Weakest preconditions for progress (Q1189258): Difference between revisions
From MaRDI portal
Set profile property. |
ReferenceBot (talk | contribs) Changed an Item |
||
Property / cites work | |||
Property / cites work: Q4692502 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4144755 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4692630 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3925859 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Temporal predicate transformers and fair termination / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Proving Liveness Properties of Concurrent Programs / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A lattice-theoretical fixpoint theorem and its applications / rank | |||
Normal rank |
Revision as of 10:33, 16 May 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Weakest preconditions for progress |
scientific article |
Statements
Weakest preconditions for progress (English)
0 references
26 September 1992
0 references
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.
0 references
weakest preconditions
0 references
progress properties
0 references