Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
This example Z specification dates from the occasion when a colleague decided he wanted to try a heart rate monitor (HRM), and organized a group of us to share the cost. The specification addresses the problem of ensuring fair usage of the HRM. - - - - - - - - - - - - - - - - - - - - - - - - --

section share parents toolkit

[Person]

There is a set of persons, not all of whom are shareholders. (We should really specify a minimum size for this set.) Conversely, all shareholders are persons. (Pets are excluded, or if you prefer are treated as persons.)


		Time == $\nat$

Times are represented by ordinal numbers.

		Share



		key : $\nat$
		last_used : Time

	$\end{schema}$

Each share has a key to distinguish it from other shares and records the time at which its bearer last used the HRM.

		State



		bearer : Share $\pfun$ Person
		location : Person

	$\end{schema}$

The state comprises a function from the born shares to persons (every share is born by one person), and a location, that is the person currently in possession of the HRM. This does not exclude one person from bearing more than one share, though we might want to reconsider this. It assumes that several people would not want to share a single share.


		instigator : Person

	InitState



	$\Delta$ State

$\where$	$\where$	$\where$

	bearer' = {( $\lblot$ key == 0, last_used == 0 $\rblot$ , instigator)}
	location' = instigator

$\end{schema}$

In the initial state, the instigator bears the sole share and has possession of the HRM.

	IssueShare



	$\Delta$ State
	new_punter? : Person

$\where$	$\where$	$\where$

	bearer' = bearer $\oplus$
	{s' : Share \| s'.key = # (dom bearer) $\land$
	s'.last_used = max {s : dom bearer s.last_used} + 1
	(s',new_punter?))
	location' = location

$\end{schema}$

A new share can be issued to a person, though in practice this will require the consent of the existing shareholders, as their shares will decrease in value as a result. The new share's timestamp is set so as to give precedence to existing shareholders. The HRM remains with whoever already had possession of it.

	AcquireShare



	$\Delta$ State
	punters? : $\power$ Person

$\where$	$\where$	$\where$

	$\forall$ p : punters?
	min {s : dom (bearer $\rres$ {location'}) s.last_used} =
	min {s : dom (bearer $\rres$ {p}) s.last_used}
	$\exists$ s : dom (bearer $\rres$ {location'})
	bearer' = bearer $\oplus$
	{ $\mu$ s' : Share \|
	s'.key = s.key $\land$
	s'.last_used = max {s2 : dom bearer s2.last_used}+1
	(s', bearer s))

$\end{schema}$

The Acquire operation defines how a conflict between a set of persons all wanting to use the HRM at the same time is resolved: the person bearing a share that shows that person to have used the HRM least recently acquires possession of the HRM. The timestamp in that share is revised. The case of only one person wishing to use the HRM at a particular time is a special case that is covered by this general operation. The case of the same person holding more than one share that have all been used less recently that those of the other persons is resolved non-deterministically: any one of those shares has its timestamp revised.

	TransferShare



	$\Delta$ State
	vendor?, purchaser? : Person
	share? : Share

$\where$	$\where$	$\where$

	(share?,vendor?) $\in$ bearer
	bearer' = bearer $\oplus$ {(share?,purchaser?)}
	location' = if location = vendor? then purchaser? else location

$\end{schema}$

Shares can be transferred from one person to another, for example when a person leaves York. If that person is currently in possession of the HRM, the HRM is also transferred to the purchaser. Whether the vendor engages in a search for a highest bidder is outside the scope of this specification. There is no operation to destroy a share; a share can simply fall into disuse. - - - - - - - - - - - - - - - - - - - - - - - - -- Postscript: the instigator left, taking the HRM with him, and then refunding the shareholders!