Name
Abstract | ||
|---|---|---|
Commands interpreted in general correctness are usually characterised by their wp and wlp predicate transformer effects. We describe a way to ascribe to such commands a single predicate transformer semantics which embodies both their wp and wlp characteristics. The new single predicate transformer describes an everywhere-terminating "lifted" computation in an ok-enriched variable space, where ok is inspired by Hoare and He's UTP but has the novelty here that it enjoys the same status as the other state variables, so that it can be manipulated directly in the lifted computation itself. The relational model of this lifted computation is not, however, simply the canonical UTP relation of the original underlying computation, since this turns out to yield too cumbersome a lifted computation to permit reasoning about efficiently with the mechanised tools available. Instead we adopt a slightly less constrained model, which we are able to show is nevertheless still effective for our purpose, and yet admits a much more efficient form of mechanised reasoning with the tools available. |
Year | Venue | Keywords |
|---|---|---|
2007 | IFM | new single predicate transformer,mechanised tool,wlp characteristic,canonical utp relation,partial correctness,wlp predicate transformer effect,relational model,single predicate transformer semantics,general correctness,efficient form,original underlying computation,mechanised reasoning |
Field | DocType | Volume |
Predicate transformer semantics,Programming language,Computer science,Correctness,Transformer,Theoretical computer science,State variable,Predicate (grammar),Novelty,Relational model,Computation | Conference | 4591 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.38 |
References | Authors | |
16 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Steve Dunne | 1 | 154 | 14.75 |
| Andy Galloway | 2 | 177 | 18.25 |