🚀 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.

cliff@cs.man.ac.uk (Cliff B Jones) writes:
>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. 

	But what is the type name for the whole type?  How do I declare a
	variable of that type? etc.

	In section 9.1 of your book your examples do not use the whole
	state.  For example your MBAG module imports and uses just the type Bag
	which is only a component of the state of the BAG module.  Your quoted
	pre/post-conditions operate on a Bag object rather than on the
	state object.  There does not appear to much of a purpose for the state
	declaration.  The same effect could be achieved with a module that
	exported only a type and functions that operated on that type.

	Then in the CDICT module you refer to LDICT.State which is the name of
	the state id of the LDICT module.  This is the heart of the matter.
	I cannot find anywhere in [Dawes] a clear statement that the state id
	is a bona fide type name of some record type, that furthermore can be
	referenced outside of the module even though it is not explicitly
	exported.

	Furthermore your example for the STORE operation in CDICT appears to 
	have an error.  From

		type Cdict = LDICT.State*

		cd : Cdict

		.... post-STOREL(i, a, hd ?cd, ld)

	I conclude that the type of the third argument of the post-condition
	must be of type LDICT.State but in actual fact it is of type Ldict, 
	the state's field type.  What if there is more than one field?  All of
	your examples only have one field.

	I would be happy to refer to a type MODULE.State and declare state
	variables of that type but then how to do I quote postconditions which
	typically refer to components of the state?  Presumably the components
	are supposed to be hidden within the module and not exported.

	I hope this clarifies my confusion.

		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.

Regards
-- 
Anthony Shipman                 "You've got to be taught before it's too late,
CP Software Export Pty Ltd,      Before you are six or seven or eight,
19 Cato St., East Hawthorn,      To hate all the people your relatives hate,
Melbourne, Australia, 3121       You've got to be carefully taught."  R&H