A prospective-value semantics for the GSL 

Hdl Handle:
http://hdl.handle.net/10149/58311
Title:
A prospective-value semantics for the GSL 
Book Title:
ZB 2005: Formal specification and development in Z and B
Authors:
Zeyda, F. (Frank); Stoddart, W. J. (Bill); Dunne, S. E. (Steve)
Editors:
Treharne, H. (Helen); King, S. (Steve); Henson, M. C. (Martin); Schneider, S. (Steve)
Affiliation:
University of Teesside. School of Computing.
Citation:
Zeyda, F., Stoddart, W. J. and Dunne, S. E. (2005) 'A prospective-value semantics for the GSL', 4th International Conference of B and Z Users. Guildford, UK, April 2005, in Treharne, H. et al. (eds) ZB 2005: Formal specification and development in Z and B. Lecture notes in computer science. Heidelberg: Springer-Verlag Berlin, pp.187-202.
Publisher:
Spinger-Verlag
Conference:
4th International Conference of B and Z Users, 2005, Guildford, UK, April 2005
Issue Date:
2005
URI:
http://hdl.handle.net/10149/58311
DOI:
10.1017/b135596
Additional Links:
http://www.springerlink.com/content/pq08c0bflxj58pm5/
Abstract:
We present a prospective-value (pv) semantics for the Generalised Substitution Language. Whereas wp semantics captures the meaning of a computation in terms of the weakest precondition that must be fulfilled for a generalised substitution S to establish any given postcondition Q, pv semantics expresses the meaning of a computation in terms of the value any expression E would take were the computation to be carried out. To integrate non-termination we formulate improper bunch theory, an extended version of Hehners bunch theory where each type is augmented with an improper bunch. Algebraic simplification laws for the pv expression transformer are presented, and proved to be sound. Iteration is treated as a fixed-point in expressions, and a corresponding theorem is presented allowing us to infer the pv effect of the while-loop construct.
Type:
Meetings and Proceedings; Book Chapter
Keywords:
generalised substitution; bunch theory; prospective-value semantics; expression transformers; wp calculus; B method
Series/Report no.:
Lecture notes in computer science; 3455
ISBN:
0302-9743

Full metadata record

DC FieldValue Language
dc.contributor.authorZeyda, F. (Frank)-
dc.contributor.authorStoddart, W. J. (Bill)-
dc.contributor.authorDunne, S. E. (Steve)-
dc.contributor.editorTreharne, H. (Helen)-
dc.contributor.editorKing, S. (Steve)-
dc.contributor.editorHenson, M. C. (Martin)-
dc.contributor.editorSchneider, S. (Steve)-
dc.date.accessioned2009-04-01T10:48:42Z-
dc.date.available2009-04-01T10:48:42Z-
dc.date.issued2005-
dc.identifier.isbn0302-9743-
dc.identifier.doi10.1017/b135596-
dc.identifier.urihttp://hdl.handle.net/10149/58311-
dc.description.abstractWe present a prospective-value (pv) semantics for the Generalised Substitution Language. Whereas wp semantics captures the meaning of a computation in terms of the weakest precondition that must be fulfilled for a generalised substitution S to establish any given postcondition Q, pv semantics expresses the meaning of a computation in terms of the value any expression E would take were the computation to be carried out. To integrate non-termination we formulate improper bunch theory, an extended version of Hehners bunch theory where each type is augmented with an improper bunch. Algebraic simplification laws for the pv expression transformer are presented, and proved to be sound. Iteration is treated as a fixed-point in expressions, and a corresponding theorem is presented allowing us to infer the pv effect of the while-loop construct.-
dc.publisherSpinger-Verlag-
dc.relation.ispartofseriesLecture notes in computer science-
dc.relation.ispartofseries3455-
dc.relation.urlhttp://www.springerlink.com/content/pq08c0bflxj58pm5/-
dc.subjectgeneralised substitution-
dc.subjectbunch theory-
dc.subjectprospective-value semantics-
dc.subjectexpression transformers-
dc.subjectwp calculus-
dc.subjectB method-
dc.titleA prospective-value semantics for the GSL -
dc.typeMeetings and Proceedings-
dc.typeBook Chapter-
dc.contributor.departmentUniversity of Teesside. School of Computing.-
dc.title.bookZB 2005: Formal specification and development in Z and B-
dc.identifier.conference4th International Conference of B and Z Users, 2005, Guildford, UK, April 2005-
ref.assessmentRAE 2008-
or.citation.harvardZeyda, F., Stoddart, W. J. and Dunne, S. E. (2005) 'A prospective-value semantics for the GSL', 4th International Conference of B and Z Users. Guildford, UK, April 2005, in Treharne, H. et al. (eds) ZB 2005: Formal specification and development in Z and B. Lecture notes in computer science. Heidelberg: Springer-Verlag Berlin, pp.187-202.-
prism.startingPage187-
prism.endingPage202-
All Items in TeesRep are protected by copyright, with all rights reserved, unless otherwise indicated.