🚀 go-pugleaf

Taking up the forum's invitation to introduce myself:

I'm Mike Poppleton at Coventry University. For my recent M.Sc. dissertation
I Z-specified an extension of the relational DB model, with specific reference
to integrity constraints.
I'm developing this spec & have some questions I would be most grateful for
feedback on.

The model is based on a collection of sets of strings, or "value types". These
(rather simplistically) model the notion of "type" in my spec:
	
	[CH]
	STRING == seq CH	
	VT : P P STRING 
A fundamental part of the model's state is the value types plus their
operations:

	|-VTypes-------------------------------------
	|vts: seq1 VT
	|f1: seq1 (STRING -+-> STRING)
	|fn: VT
	|<...functions of other arity, other components...>
	|--------------------------------------------
	|<...constraints>
	|--------------------------------------------
OK so far, in fact no need for more than an axiomatic definition of VTypes.
However - question 1: can I make my value types (string sets) & more 
specifically their operations into data? i.e. can functions be input as data:

	|-CreateVTypes-------------------------------
	|DELTA VTypes
	|vts?: seq1 VT
	|f1?: seq1 (STRING -+-> STRING)
	|<..input functions of other arity...>
	|--------------------------------------------
	|vts' = vts?
	|f1' = f1?
	|<...etc>
	|--------------------------------------------
Question 2: is it then legal to "instantiate" and use the value types as
the basis for the rest of the state definition, i.e.:

	vt: VTypes

	| X: P (vt.fn x STRING)			
	|--------------------------------------------
	| X = {set comprehension using vt.fn & STRING}
	
	<...etc...>
A form of "initial state existence" proof obligation for CreateVTypes 
looks straightforward. My spec continues to build global definitions,
and state schema assuming that vt has been sensibly user-input (of course
begging any implementation questions).
  
To move onto a more substantial question of nested state schema & associated
operations. I define a 3-deep nest:

	|-SSub2----	|-SSub1--------		|-S-------------
	|<...>		|c11:SSub2		|c01: F SSub1	<finite subset>
	|----------	|c12:<...>		|c02:<....>
	|<...>		|--------------		|--------------
	|----------	|<.....>		|<...>
	           	|--------------		|--------------
Initial state schemas:using THETA is OK as long as its argument defines
precisely ONE schema situation (as I understand it):

	|-InitSSub2----		|-InitSSub1--------	|-InitS---------------	
	|SSub2'			|SSub1'			|S'
	|--------------		|InitSSub2		|InitSSub1'
	|<assignments...>	|------------------	|---------------------
	|--------------		|c11'=THETA SSub2'	|c01'={THETA SSub1'}
				|<assignements...>	|<assignments...>	
	           		|------------------	|---------------------
Operation schemas:say we have various ops for SSub2, say SSub2Op1...SSub2Opn.
How then to incorporate the desired SSub2 after-state into a SSub1 operation?
e.g.
	|-SSub1Create----------
	|DELTA SSub1			
	|<SSub2-expr>
	|<inputs for other
	|     components >
	|----------------------
	|c11' = THETA SSub2'
	|<....>
	|----------------------
<SSub2-expr> should uniquely define the SSub2' situation in order that the
THETA expression is sensible. Clearly the most general expression:
	SSub2'
doesn't satisfy this. A "SSub2 disjunction operation" SSub2OpDis where
	SSub2OpDis ISDEF SSub2Create \/ SSub2Op1 \/ ... \/ SSub2Opn
doesn't look very deterministic either.

Furthermore the problem is even harder for top-level state schema S, which 
has a finite set of SSub1's in it.
Comments/ advice gratefully received, also any references to Z-specifications
that do this sort of modular structuring. Thanks for your time.

Mike Poppleton, Computer Science Dept., Coventry University
mikep@uk.ac.coventry
Mon 27/7/92