🚀 go-pugleaf

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