Achieving Temporal Liveness and Safety in Prolog

[jeffrose]

... or How to Write Leakproof Programs Without Really Trying :-)

All:

Some of you may know that I am rather fond of what might be called an "unusual" use of setup_call_cleanup/3. I have found this control structure to be so powerful, so versatile, and its use-cases so compelling as to be worthy of an operator. I defined the operator '~>' to mean "eventually implies". It is analogous to the "leads-to" operator of Owicki and Lamport, 1982. There's a citation in the attachment.

Attached are five examples: Mutual Exclusion, Joining Several Threads, Socket Programming, Verifying Calculations, and finally, Dijkstra's Dining Philosophers.

It is very exciting. What do you think?

Regards,
Jeff R.