refinement notions in Z and VDM

Article View: comp.specification.z

Article #38

Back to comp.specification.z Previous Next

#38

From: 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    |
+--------------------------------------------------------------+

Technical Details

Message-ID: <8665@samson.informatik.uni-kiel.dbp.de>

Path: arc1-ca.pugleaf.net!sparky!uunet!mcsun!unido!majestix!khb

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!sparky!uunet!mcsun!unido!majestix!khb
From: khb@informatik.uni-kiel.dbp.de (Karl-Heinz Buth)
Newsgroups: comp.specification.z
Subject: refinement notions in Z and VDM
Keywords: refinement, Z, VDM
Message-ID: <8665@samson.informatik.uni-kiel.dbp.de>
Date: 9 Apr 92 08:50:16 GMT
Organization: Dept. of Computer Science, University of Kiel, FRG
Lines: 21