\input zb-basic
\input zb-ioport
\iteman{io-port 00683357}
\itemau{Larsen, Peter Gorm}
\itemti{Towards proof rules for looseness in explicit definitions from VDM-SL.}
\itemso{Andrews, Derek J. (ed.) et al., Semantics of specification languages (SoSL). Proceedings of the International Workshop, Utrecht, the Netherlands, 25-27 October 1993. Berlin: Springer-Verlag. Workshops in Computing. 118-134 (1994).}
\itemab
Summary: The model-oriented formal method called VDM contains a specification language called VDM-SL. This language existed in a number of different dialects, but now a standard for the language has been prepared, including a dynamic semantics defined from a model-theoretic point of view. Thus, it is not at all clear that the defined semantics is appropriate for deriving proof rules which reflect the semantics. This paper focus on the possible ways of defining proof rules which reflects the semantics of explicit definitions which contain looseness. The model-theoretic view which has been chosen for the definition of the semantics for VDM-SL, incorporates looseness by denoting the semantics of a (loose) specification as a set of models. The proof system should be designed such that properties which can be proved about a given specification should hold for all its models. This paper shows why it is an interesting challenge to develop a proof system which are able to do this.
\itemrv{~}
\itemcc{}
\itemut{specification language; dynamic semantics}
\itemli{}
\end