🚀 go-pugleaf

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 can import types, values, functions and operations from a module but what do
I do with the state?

Suppose I have a module with a state of many fields and a collection of
operations that operate on various combinations of those fields.  Then in
another module I want to create a variable of the ADT implemented by the
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 book talks about a notional record type associated with the state but seems
to imply that the type cannot be named or used explicitly yet there is a state
id available to name it.

I would like to have a module that is not an ADT but contains state variables
that are acted on from outside by calling the exported operations.  Is this
possible?  How do I write the post-conditions of such operations in the 
calling module?

The 'using' clause seems to provide a mechanism to operate on state variables.
But it includes a state designator which the book explains as defining "a
record of the same type as the notional state type of the module containing the
definition of Op".  How do I make such an object?  Surely it means
'designating' rather than 'defining' anyway?

It seems that I can only use 'using' with calls to explicitly 
defined operations.  What do I do about implicitly defined operations?

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

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