🚀 go-pugleaf

In article <1992Aug21.130630.4998@bohra.cpg.oz.au> als@bohra.cpg.oz.au (Anthony Shipman) writes:
>I have been trying to come to grips with modules and state as described
>in "The VDM-SL Reference Guide" by Dawes and now I'm thoroughly confused.
>

I rate John Dawes' book on VDM-SL as very useful but the material on
modules could be improved!

>I can import types, values, functions and operations from a module but what do
>I do with the state?
>
>Suppose I have a module ...
>
>What is the type that I use for the variable?  
>How do I use the post-condition of an operation from the imported module if its
>signature refers to fields of the state but I only have a single variable 
>containing the state?
>

The whole idea of the module in VDM is that it is a "closed" object
which can only be manipulated via operations which are exported. It is
therefore reasonable that the only "type" which is generated is for
the whole state. In fact, the story is a bit more complicated because
- assuming that the (operations of the) importing module are specified
implicitly - one cannot "invoke" operations from a logical expression.
This problem is overcome by permitting the "quoting" of
pre/post-conditions.

>
>Is there a better explanation of modules (outside of the standard)?
>

You might get some idea from the examples in Section 9.1 of
	
@book{Jones90a,
	author	    =	"C.~B.~Jones",
	title	    =	"Systematic Software Development using VDM",
	edition =	{Second},
	publisher   =	"Prentice Hall International",
	year	    =	"1990",
	length =	"333 pages"
}

>While I'm at it how come function types have to be duplicated
>in import and export module signatures all over the place?  In a spec of
>practical (non-academic) size one change to a function may mean editing
>a large number of modules.  If readability is a concern then a listing
>from a CASE tool can include the duplicated signatures. The info is 
>mechanically derivable so I shouldn't have to do it.
>-- 
I'm inclined to your view here - but those on the committee who voted
for the more verbose versions could also point out that the redundant
material could be generated by tools!

cliff jones

PS
In a later posting, you ask about the status of modules in the
standard (a draft of which is being sent out right now). The current
position is that they will be presented in an "informative"
("non-normative") Appendix. The argument for this is that while
"flat-VDM" has been extensively used, the same is not true for the
module concept. There is much debate in general (I don't think any
specification language could claim to have solved all of the problems)
and in the VDM community in particular about the role of
modularization. See for example the papers in the "Formal Aspects of
Computing" Vol 4, No 1, 1992.