Weakest preconditions for progress (Q1189258): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
(One intermediate revision by one other user not shown) | |||
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 | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/bf01212336 / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2101027003 / rank | |||
Normal rank |
Latest revision as of 11:48, 30 July 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