Weakest precondition
by
Manuel Carro
—
last modified
Apr 25, 2012 14:36
—
filed under:
KnowledgeModel
Definitions
| Term: term |
Domain: Cross-cutting issues | ||||
|---|---|---|---|---|---|
| Engineering and Design (KM-ED) |
Adaptation and Monitoring (KM-AM) |
Quality Definition, Negotiation and
Assurance (KM-QA) |
Generic (domain independent) |
||
| D o m a i n : L a y e r s |
Business Process Management (KM-BPM) |
||||
| Service Composition and
Coordination (KM-SC) |
For a set of actions S (which can be a service composition)
and a formal (e.g., logical) statement Q describing the state after
executing S, a precondition P is a formal description of the state
before executing S such that when P is fulfilled, so is Q. The weakest
precondition is implied by any other precondition, i.e., it is true
whenever other precondition is true. Thus, it can be construed as the
most general precondition that imposes minimal constraints on the
initial state, while still ensuring that Q holds after executing S
[Doherty & Lukaszewiczy, 2001], [Dijkstra, 1975]. |
||||
| Service Infrastructure (KM-SI) |
|||||
| Generic (domain independent) |
|||||
Competencies
- UoC: Service Specification; http://www.uoc.gr; George Baryannis, Dimitris Plexousakis.
- UPM: Seervice Specification; http://www.upm.es; Manuel Carro.
References
- [Doherty & Lukaszewiczy, 2001] Patrick Doherty, Witold Łukaszewiczy: Computing Strongest Necessary and Weakest Sufficient Conditions of First-Order Formulas. In Proceedings of the 17th Int’l Joint Conference on Artificial Intelligence, August 4th-10th, 2001, Seattle, Washington, USA (IJCAI- 2001).
- [Dijkstra, 1975] Guarded Commands, Nondeterminacy and Formal Derivation of Programs. E. W. Dijkstra. Communications of the ACM. Vol. 18, Num. 8, Aug. 1975.
