specification languages and TSL

specification languages and TSL

[Doug Bryan]

A few issues back, David Guaspari wrote that though TSL can be used
to specify the order of rendezvous, it doesn't allow for specifying
the data exchanged during a rendezvous.  This is not true.

TSL (Task Sequencing Language) has been around since 1985.  It is an
annotation languages designed specifically for the tasking constructs
of Ada.  TSL allows you to state the intended interactions between
tasks, e.g.:

	task type Semaphore is
	  entry Seize;
	  entry Release;
	  --+ when ?S accepts ?U at Seize then
	  --+   ?S accepts ?U at Release
	  --+ until ?S accepts any;
	end Semaphore;

This specifies that when a semaphore task starts a rendezvous at
Seize with some user ?U, then its next rendezvous must be with
that same user at Release.

The intended data exchanged during rendezvous can also be specified:

	task type Queue is
	  entry Enqueue (I : Item);
	  entry Dequeue (I : out Item);
	  --+ when ?Q accepts any at Enqueue (?I) then
	  --+    ?Q releases any from Deqeueu (?I);
	end Queue;

Here we specify that when a value ?I is enqueued to the task ?Q, the
value must be dequeued before the queue task ?Q terminates.

TSL also has features for abstracting program state and abstracting
actions performed by tasks.

doug