Lifting general correctness into partial correctness is OK

Hdl Handle:
http://hdl.handle.net/10149/58309
Title:
Lifting general correctness into partial correctness is OK
Book Title:
Integrated formal methods
Authors:
Dunne, S. E. (Steve); Galloway, A. J. (Andy)
Editors:
Davies, J. (Jim); Gibbons, J. (Jeremy)
Affiliation:
University of Teesside. School of Computing; University of York. Department of Computer Science. High Integrity Systems Engineering.
Citation:
Dunne, S. E. and Galloway, A. J. (2007) 'Lifting general correctness into partial correctness is OK', Integrated formal methods (IFM) 6th International Conference, Oxford, UK, July 2-5, 2007, in Davies, J. and Gibbons, J. (eds) Integrated formal methods, Lecture notes in computer science. Heidelburg: Springer Berlin, pp.215-232.
Publisher:
Springer Berlin / Heidelberg
Conference:
Integrated formal methods (IFM) 6th International Conference, 2007, Oxford, UK, July 2-5, 2007.
Issue Date:
2007
URI:
http://hdl.handle.net/10149/58309
DOI:
10.1007/978-3-540-73210-5_12
Additional Links:
http://www.springerlink.com/content/r272426516125g52/
Abstract:
Commands interpreted in general correctness are usually characterised by their wp and wlp predicate transformer effects. The authors 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.
Type:
Meetings and Proceedings; Book Chapter
Keywords:
general correctness; wp; wlp; single predicate transformer semantics; Hoare and He
Series/Report no.:
Lecture notes in computer science; 4591
Citation Count:
0 [Web of Science and Scopus, 20/01/2010]

Full metadata record

DC FieldValue Language
dc.contributor.authorDunne, S. E. (Steve)-
dc.contributor.authorGalloway, A. J. (Andy)-
dc.contributor.editorDavies, J. (Jim)-
dc.contributor.editorGibbons, J. (Jeremy)-
dc.date.accessioned2009-04-01T10:48:39Z-
dc.date.available2009-04-01T10:48:39Z-
dc.date.issued2007-
dc.identifier.doi10.1007/978-3-540-73210-5_12-
dc.identifier.urihttp://hdl.handle.net/10149/58309-
dc.description.abstractCommands interpreted in general correctness are usually characterised by their wp and wlp predicate transformer effects. The authors 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.-
dc.publisherSpringer Berlin / Heidelberg-
dc.relation.ispartofseriesLecture notes in computer science-
dc.relation.ispartofseries4591-
dc.relation.urlhttp://www.springerlink.com/content/r272426516125g52/-
dc.subjectgeneral correctness-
dc.subjectwp-
dc.subjectwlp-
dc.subjectsingle predicate transformer semantics-
dc.subjectHoare and He-
dc.titleLifting general correctness into partial correctness is OK-
dc.typeMeetings and Proceedings-
dc.typeBook Chapter-
dc.contributor.departmentUniversity of Teesside. School of Computing; University of York. Department of Computer Science. High Integrity Systems Engineering.-
dc.title.bookIntegrated formal methods-
dc.identifier.conferenceIntegrated formal methods (IFM) 6th International Conference, 2007, Oxford, UK, July 2-5, 2007.-
ref.assessmentRAE 2008-
ref.citationcount0 [Web of Science and Scopus, 20/01/2010]-
or.citation.harvardDunne, S. E. and Galloway, A. J. (2007) 'Lifting general correctness into partial correctness is OK', Integrated formal methods (IFM) 6th International Conference, Oxford, UK, July 2-5, 2007, in Davies, J. and Gibbons, J. (eds) Integrated formal methods, Lecture notes in computer science. Heidelburg: Springer Berlin, pp.215-232.-
prism.startingPage215-
prism.endingPage232-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.