refinement notions in Z and VDM

Thread View: comp.specification.z

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by Karl-Heinz Buth Thu, 09 Apr 1992 08:50

#38

Author: Karl-Heinz Buth
Date: Thu, 09 Apr 1992 08:50

21 lines
1478 bytes

Currently, I am investigating the relation between the refinement
notions in VDM and Z. After having read Cliff Jones' book on VDM and
Mike Spivey's reference manual on Z, it seems to me that there is not
much of a difference. After translation into the other formalism, the
proof obligations look essentially the same. Since I am not so very
experienced in Z, I would like the Z community to comment on this. Am
I right, or are there fundamental differences between Z and VDM in
this area?

I know that there has been quite some discussion on Z vs. VDM on the
net during last year. But this was mostly on other aspects like
usability, and not so much on theoretical foundations.


Karl-Heinz Buth
+--------------------------------------------------------------+
|  Institut fuer Informatik, Christian-Albrechts-Universitaet  |
|          Preusserstr. 1-9, W-2300 Kiel 1, Germany            |
|        Tel.: ++49-431-560421  Fax: ++49-431-566143           |
|   E-mail: khb@causun.uucp, khb@informatik.uni-kiel.dbp.de    |
+--------------------------------------------------------------+

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads