For non-terminating programs I use processes as described by Tony Hoare in "Communicating Sequential Processes". Procedures must always terminate in Albatross.

For non-terminating programs I use processes as described by Tony Hoare in "Communicating Sequential Processes". Procedures must always terminate in Albatross. If I have more documentation on aliasing, I can give you hint. Could you provide me some email address?