Back to Search Start Over

Floyd-Hoare Logic

Authors :
Stephen L. Bloom
Zoltán Ésik
Source :
Iteration Theories ISBN: 9783642780363
Publication Year :
1993
Publisher :
Springer Berlin Heidelberg, 1993.

Abstract

Suppose that f: Q → Q is a partial function on a set Q, where we might think of Q as a set of “states” of a machine. If α and β are predicates on Q, i.e. total maps Q → {TRUE, FALSE}, partial correctness assertion {α} f {β}, pca for short, means $$ \forall q \in Q\left[ {\alpha \left( q \right) = {\text{TRUE}}\, \wedge f\left( q \right){\text{defined}}\, \Rightarrow \beta \left( {f\left( q \right) = {\text{TRUE}}} \right)} \right] $$ .

Subjects

Subjects :
Combinatorics
Physics
Hoare logic

Details

ISBN :
978-3-642-78036-3
ISBNs :
9783642780363
Database :
OpenAIRE
Journal :
Iteration Theories ISBN: 9783642780363
Accession number :
edsair.doi...........c42fbf443d84f882178d35389128a9f1