A Precise Semantics for Ultraloose Specifications
[pdf]
Glasgow, Scotland
1993
Abstract
All formal specifiers face the danger of overspecification: accidentally writing an overly restrictive specification. This problem is particularly acute for axiomatic specifications because it is so easy to write axioms that hold for some of the intended implementations but not for all of them (or, rather, it is hard not to write overly strong axioms).
One of the best developed ways of recovering some of these implementations which do not literally satisfy the specification is to apply a ``behavioural abstraction operator'' to a specification: adding in those implementations which have the same ``behaviour'' as an implementation which does satisfy the specification.
In two recent papers, Broy and Wirsing propose an alternative (and apparently simpler) approach which they call ``ultraloose specification.'' This approach is based on a particular style of writing axioms which avoids certain forms of overspecification.
An important, unanswered question is ``How does the ultraloose approach relate to other solutions?'' The major achievement of this thesis is a proof that the ultraloose approach is semantically equivalent to the use of the ``behavioural abstraction operator.'' This result is rather surprising in the light of a result by Schoett which seems to say that such a result is impossible.
BibTeX
@mastersthesis{ReidThesis93 , abstract = { All formal specifiers face the danger of overspecification: accidentally writing an overly restrictive specification. This problem is particularly acute for axiomatic specifications because it is so easy to write axioms that hold for some of the intended implementations but not for all of them (or, rather, it is hard not to write overly strong axioms).One of the best developed ways of recovering some of these implementations which do not literally satisfy the specification is to apply a ``behavioural abstraction operator'' to a specification: adding in those implementations which have the same ``behaviour'' as an implementation which does satisfy the specification.
In two recent papers, Broy and Wirsing propose an alternative (and apparently simpler) approach which they call ``ultraloose specification.'' This approach is based on a particular style of writing axioms which avoids certain forms of overspecification.
An important, unanswered question is ``How does the ultraloose approach relate to other solutions?'' The major achievement of this thesis is a proof that the ultraloose approach is semantically equivalent to the use of the ``behavioural abstraction operator.'' This result is rather surprising in the light of a result by Schoett which seems to say that such a result is impossible. } , affiliation = {University of Glasgow} , ar_file = {MSc_93} , ar_shortname = {MSc 93} , author = {Alastair Reid} , file = {ReidThesis93.pdf} , location = {Glasgow, Scotland} , png = {ReidThesis93.png} , school = {Glasgow School of Computing Science} , title = {{A} Precise {S}emantics for {U}ltraloose {S}pecifications} , year = {1993} }